Nicolas Halbwachs
Mathias Péron
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 AI; the new idea is to consider relational abstract properties ψ(AI, BI, ...) 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.
- 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.Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI 2003, ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, pages 196--207, San Diego (Ca.), June 2003. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In J. Ferrante and K. S. McKinley, editors, PLDI 2007, pages 300--309. ACM, 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd Int. Symp. on Programming. Dunod, Paris, 1976.Google Scholar
- R. C. Claris and J. Cortadella. Verification of parametric timed circuits using octahedra. In Designing correct circuits, DCC'04, Barcelona, March 2004.Google Scholar
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978. Google ScholarDigital Library
- 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.Google Scholar
- D. L. Dill. Timing assumptions and verification of finite state concurrent systems. In Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, June 1989. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL 2002, pages 191--202. ACM, 2002. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- D. Gopan. Numeric program analysis techniques with applications to array analysis and library summarization. PhD thesis, Computer Science Department, University of Wisconsin, Madison, WI, August 2007. Google ScholarDigital Library
- D. Gopan, T. Reps, and M. Sagiv. A framework for numeric analysis of array operations. In Proc. of POPL'2005, pages 338 -- 350, Long Beach, CA, 2005. Google ScholarDigital Library
- C. A. R. Hoare. Proof of a program: Find. CACM, 14(1):39--45, 1971. Google ScholarDigital Library
- R. Iosif, P. Habermehl, and T. Vojnar. What else is decidable about arrays? In R. Amadio, editor, FOSSACS 2008. LNCS, Springer Verlag, 2008. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google Scholar
- F. Masdupuy. Array abstractions using semantic analysis of trapezoid congruences. In ICS '92: Proceedings of the 6th international conference on Supercomputing, pages 226--235, New York, NY, USA, 1992. ACM. Google ScholarDigital Library
- A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310--319. IEEE CS Press, October 2001. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Discovering properties about arrays in simple programs
Recommendations
Discovering properties about arrays in simple programs
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationArray 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 ...
Invariant Synthesis for Programs Manipulating Arrays with Unbounded Data
Internetware '15: Proceedings of the 7th Asia-Pacific Symposium on InternetwareThis paper proposes a way of using abstract interpretation for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple loops. The method summarizes an array property as an interval property. ...
Defunctionalizing push arrays
FHPC '14: Proceedings of the 3rd ACM SIGPLAN workshop on Functional high-performance computingRecent work on embedded domain specific languages (EDSLs) for high performance array programming has given rise to a number of array representations. In Feldspar and Obsidian there are two different kinds of arrays, called Pull and Push arrays. Both ...
Comments