Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

Array bound checking and array dependency analysis (for parallelization) have been widely studied. However, there are much less results about analyzing properties of array contents. In this paper, we propose a way of using abstract interpretation for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple "for" loops. The basic idea, borrowed from [GRS05], consists in partitioning arrays into symbolic intervals (e.g., [1,i -- 1], [i,i], [i + 1,n]), and in associating with each such interval I and each array A an abstract variable A_I; the new idea is to consider relational abstract properties ψ(A_I, B_I, ...) about these abstract variables, and to interpret such a property pointwise on the interval I: ∀l ∈ I, ψ(A[l], B[l],...). The abstract semantics of our simple programs according to these abstract properties has been defined and implemented in a prototype tool. The method is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a "sentinel", the index stays within the bounds.

REFERENCES

• 1: R. Alur, C. Courcoubetis, and D. L. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2--34, 1993. Preliminary version appears in the Proc. of 5th LICS, 1990.
• 2: A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In Computer Aided Verification (CAV 2006), pages 517--531. LNCS 4144, Springer Verlag, July 2006.
• 3: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 4: 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
• 5: S. Bardin, J. Leroux, and G. Point. Tool presentation: Fast extended release. In 18th Conf. Computer Aided Verification (CAV'2006), pages 63--66, Seattle (Washington), 2006. LNCS 4144, Springer-Verlag.
• 6: A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? In E. A. Emerson and K. S. Namjoshi, editors, VMCAI 06, pages 427--442. LNCS 3855, Springer Verlag, 2006.
• 7: P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd Int. Symp. on Programming. Dunod, Paris, 1976.
• 8: R. C. Claris and J. Cortadella. Verification of parametric timed circuits using octahedra. In Designing correct circuits, DCC'04, Barcelona, March 2004.
• 9: 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]
• 10: P. Cousot. Verification by abstract interpretation. In N. Dershowitz, editor, Proc. Int. Symp. on Verification - Theory & Practice - Honoring Zohar Manna's 64th Birthday, pages 243--268, Taormina, Italy, June 29 - July 4 2003. (c) Springer-Verlag, Berlin, Germany.
• 11: D. L. Dill, Timing assumptions and verification of finite-state concurrent systems, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.197-212, February 1990, Grenoble, France
• 12: 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
• 13: D. Gopan, F. Di Maio, N. Dor, T. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In TACAS'04, pages 512--529, Barcelona, 2004.
• 14: S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified logical domains. In G. C. Necula and P. Wadler, editors, POPL 2008, pages 235--246. ACM, 2008.
• 15: Denis Gopan , Thomas W. Reps, Numeric program analysis techniques with applications to array analysis and library summarization, University of Wisconsin at Madison, Madison, WI, 2007
• 16: 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
• 17: C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
• 18: R. Iosif, P. Habermehl, and T. Vojnar. What else is decidable about arrays? In R. Amadio, editor, FOSSACS 2008. LNCS, Springer Verlag, 2008.
• 19: R. Jhala and K. L. McMillan. Array abstractions from proofs. In W. Damm and H. Hermanns, editors, CAV 2007, pages 193--206. LNCS 4590, Springer Verlag, 2007.
• 20: S. K. Lahiri and R. E. Bryant. Indexed predicate discovery for unbounded system verification. In R. Alur and D. Peled, editors, CAV 2004, pages 135--147. LNCS 3114, Springer Verlag, 2004.
• 21: S. K. Lahiri, R. E. Bryant, and B. Cook. A symbolic approach to predicate abstraction. In W. A. Hunt Jr. and F. Somenzi, editors, CAV 2003, pages 141--153. LNCS 2725, Springer Verlag, 2003.
• 22: François Masdupuy, Array abstractions using semantic analysis of trapezoid congruences, Proceedings of the 6th international conference on Supercomputing, p.226-235, July 19-24, 1992, Washington, D. C., United States [doi>10.1145/143369.143414]
• 23: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 24: M. Péron and N. Halbwachs. An abstract domain extending Difference-Bound Matrices with disequality constraints. In B. Cook and A. Podelski, editors, 8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07, Nice, France, January 2007.

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:
Theory, Verification

Keywords:
"sentinel", abstract interpretation, arrays, invariant synthesis, program verification, sorting algorithms