Lifting abstract interpreters to quantified logical domains

ABSTRACT

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤ i < n ⇒ α[i] = 0). The principal challenge in this effort is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation. We present an automatic technique to convert the standard over-approximation operations provided with all domains into sound under-approximations. We establish the correctness of our abstract interpreters by identifying two lattices---one that establishes the soundness of the abstract interpreter and another that defines its precision, or completeness. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.

REFERENCES

• 1: Dirk Beyer , Thomas A. Henzinger , Rupak Majumdar , Andrey Rybalchenko, Path invariants, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 2: Jesse D. Bingham and Zvonimir Rakamaric. A logic and decision procedure for predicate abstraction of heap-manipulating programs. In VMCAI, pages 207--221, 2006.
• 3: A.R. Bradley, Z. Manna, and H. Sipma. What's decidable about arrays? In VMCAI, volume 3855 of LNCS, pages 427--442. Springer, 2006.
• 4: P. Cerny. Verification par interpretation abstraite de predicats parametriques. Master's thesis, Univ. Paris VII & Ecole normale superieure, Paris 20, 2003.
• 5: Patrick Cousot. Verification by abstract interpretation. In Verification: Theory and Practice, volume 2772 of LNCS, pages 243--268, 2003.
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 8: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 9: Denis Gopan , Thomas Reps , Mooly Sagiv, A framework for numeric analysis of array operations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.338-350, January 12-14, 2005, Long Beach, California, USA
• 10: Sumit Gulwani , Ashish Tiwari, Combining abstract interpreters, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 11: Sumit Gulwani and Ashish Tiwari. Static analysis of heap manipulating low-level software. In CAV, LNCS, 2007.
• 12: Sumit Gulwani, Bill McCloskey, and Ashish Tiwari. Lifting abstract interpreters to quantified logical domains. Technical Report MSR-TR-2007-87, Microsoft Research, July 2007.
• 13: Ranjit Jhala and Ken McMillan. Array abstractions from proofs. In CAV, 2007.
• 14: Michael Karr. Affine relationships among variables of a program. In Acta Informatica, pages 133--151. Springer, 1976.
• 15: Shuvendu K. Lahiri and Randal E. Bryant. Indexed predicate discovery for unbounded system verification. In CAV, pages 135--147, 2004.
• 16: Matthew Might, Logic-flow analysis of higher-order programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Theory, Verification

Keywords:
abstract interpreter, logical lattices, quantified invariants, underapproximation algorithms