David P. Monniaux
ABSTRACT
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests.
In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. Our algorithms are based on new quantifier elimination and symbolic manipulation techniques.
Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation.
The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming.
- Roberto Bagnara, Patricia M. Hill, Elena Mazzi, and Enea Zaffanella. Widening operators for weakly-relational numeric abstractions. In Static Analysis (SAS), volume 3672 of LNCS, pages 3--18. Springer, 2005. DOI: 10.1007/11547662_3. Google Scholar
Digital Library
- Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella. Precise widening operators for convex polyhedra. Sci. Comput. Program., 58 (1-2): 28--56, 2005. DOI: 10.1016/j.scico.2005.02.003. Google ScholarDigital Library
- Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The Parma Polyhedra Library, version 0.9, 2006. URL http://www.cs.unipr.it/ppl.Google Scholar
- Gogul Balakrishnan and Thomas Reps. Analyzing memory accesses in x86 executables. In Compiler Construction (CC), volume 2985 of LNCS, pages 5--23. Springer, 2004. DOI: 10.1007/b95956.Google ScholarCross Ref
- Miné, Monniaux, and Rival}BlanchetCousotEtAl02-NJ Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Design and implementation of a special-purpose static programDesign and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity, Analysis, Transformation, number 2566 in LNCS, pages 85--108. Springer, 2002. DOI: 10.1007/3-540-36377-7_5. Google Scholar
- Miné, Monniaux, and Rival}ASTREE_PLDI03 Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A static analyzer for large safety-critical software. In Programming Language Design and Implementation (PLDI), pages 196--207. ACM, 2003. DOI: 10.1145/781131.781153. Google ScholarDigital Library
- François Bourdoncle. Sémantique des langages impératifs d'ordre supérieur et interprétation abstraite. PhD thesis, École polytechnique, Palaiseau, 1992.Google Scholar
- Aaron R. Bradley and Zohar Manna The Calculus of Computation: Decision Procedures with Applications to Verification Springer, October 2007. Google ScholarDigital Library
- Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John A. Plaice. LUSTRE: a declarative language for real-time programming. In Principles of Programming Languages (POPL), pages 178--188. ACM, 1987. DOI: 10.1145/41625.41641. Google ScholarDigital Library
- Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis, and Peter Niebert. From Simulink to Scade/Lustre to TTA: a layered approach for distributed embedded applications. SIGPLAN notices, 38 (7): 153--162, 2003. DOI: 10.1145/780731.780754. Google ScholarDigital Library
- CAV05. Computer Aided Verification (CAV), number 4590 in LNCS, 2005. Springer. DOI: 10.1007/b138445.Google Scholar
- Robert Clarisó and Jordi Cortadella. The octahedron abstract domain. In Static Analysis (SAS), number 3148 in LNCS, pages 312--327. Springer, 2004.Google Scholar
- Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. Linear invariant generation using non-linear constraint solving. pages 420--433. Springer, 2003.Google Scholar
- Patrick Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI_2005, pages 1--24. DOI: 10.1007/b105073. Google ScholarCross Ref
- Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. J. of Logic Programming, 13 (2-3): 103--179, 1992. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.Google Scholar
- Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program.In Principles of Programming Languages (POPL), pages 84--96.ACM, 1978. DOI: 10.1145/512760.512770. Google ScholarDigital Library
- Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer. In Programming Languages and Systems (ESOP), number 3444 in LNCS, pages 21--30, 2005. Google ScholarDigital Library
- ESOP07. Programming Languages and Systems (ESOP), volume 4421 of LNCS, 2007. DOI: 10.1007/978-3-540-71316-6.Google Scholar
- Jeanne Ferrante and Charles Rackoff. A decision procedure for the first order theory of real addition with SIAM Journal of Computation, 4 (1): 69--76, March 1975.Google Scholar
- Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of Presburger arithmetic. In Complexity of Computation, number 7 in SIAM-AMS proceedings, pages 27--42. American Mathematical Society, 1974.Google Scholar
- Stéphane Gaubert, Éric Goubault, Ankur Taly, and Sarah Zennou. Static analysis by policy iteration on relational domains. In ESOP_2007, pages 237--252. DOI: 10.1007/978-3-540-71316-6. Google Scholar
- Thomas Gawlitza and Helmut Seidl. Precise fixpoint computation through strategy iteration. In ESOP_2007, pages 300--315. DOI: 10.1007/978-3-540-71316-6_21. Google Scholar
- Laure Gonnord and Nicolas Halbwachs. Combining widening and acceleration in linear relation analysis. In Static Analysis (SAS), volume 4134 of LNCS, pages 144--160. Springer, 2006. DOI: 10.1007/11823230_10. Google ScholarDigital Library
- Denis Gopan and Thomas W. Reps. Lookahead widening. In Computer Aided Verification (CAV), volume 4144 of LNCS, pages 452--466. Springer, 2006. DOI: 10.1007/11817963_41. Google ScholarDigital Library
- Denis Gopan and Thomas W. Reps. Low-level library analysis and summarization. In Computer Aided Verification (CAV), volume 4590 of LNCS, pages 68--81. Springer, 2007. DOI: 10.1007/978-3-540-73368-3_10. Google ScholarCross Ref
- Venkatesan}Gulwani_PLDI08 Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Program analysis as constraint solving. In Programming Language Design and Implementation (PLDI). ACM, 2008. DOI: 10.1145/1375581.1375616. Google ScholarDigital Library
- Nicolas Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. PhD thesis, Université scientifique et médicale de Grenoble, 1979.Google Scholar
- IEEE standard for Binary floating-point arithmetic for microprocessor systems. IEEE, 1985. ANSI/IEEE Std 754--1985.Google Scholar
- Bertrand Jeannet. Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design, 23 (1): 5--37, July 2003. Google ScholarDigital Library
- Deepak Kapur. Automatically generating loop invariants using quantifier elimination. In ACA (Applications of Computer Algebra), 2004.Google Scholar
- Akash Lal, Gogul Balakrishnan, and Thomas Reps. Extended weighted pushdown systems. In CAV_2005, pages 343--357. DOI: 10.1007/11817963_32. Google ScholarDigital Library
- Francesco Logozzo and Manuel Fähndrich. On the relative completeness of bytecode analysis versus source code analysis. In Compiler Construction (CC), volume 4959 of LNCS, pages 197--212. Springer, 2008. DOI: 10.1007/978-3-540-78791-4_14. Google Scholar
- Zohar Manna and John McCarthy. Properties of programs and partial function logic. In Machine Intelligence, 5, pages 27--38. Edinburgh UniversityGoogle Scholar
- Zohar Manna and Amir Pnueli. Formalization of properties of functional programs.J. ACM, 17 (3): 555--569, 1970. DOI: 10.1145/321592.321606. Google ScholarDigital Library
- Ferdinand}DBLP:conf/cc/MartinAWF98 Florian Martin, Martin Alt, Reinhard Wilhelm, and Christian Ferdinand. Analysis of loops. In Compiler Construction (CC), volume 1383 of LNCS, pages 80--94. Springer, 1998.Google ScholarCross Ref
- Antoine Miné. The octagon abstract domain. In Reverse Engineering (WCRE), pages 310--319. IEEE, 2001. DOI: 10.1109/WCRE.2001.957836. Google ScholarCross Ref
- Relational abstract domains for the detection of floating-point run-time errors. In Programming Languages and Systems (ESOP), volume 2986 of LNCS, pages 3--17. Springer, 2004.Google ScholarCross Ref
- David Monniaux. Compositional analysis of floating-point linear numerical filters. In CAV_2005, pages 199--212. DOI: 10.1007/b138445. Google ScholarCross Ref
- David Monniaux. A quantifier elimination algorithm for linear real arithmetic. In LPAR (Logic for Programming, Artificial Intelligence, and Reasoning), LNCS. Springer, 2008. Google ScholarDigital Library
- David Monniaux. Optimal abstraction on real-valued programs. In Static analysis (SAS), number 4634 in LNCS, pages 104--120. Springer, 2007. DOI: 10.1007/978-3-540-74061-2_7. Google Scholar
- David Monniaux. The pitfalls of verifying floating-point computations. ACM Transactions on programming languages and systems, ACM Transactions on programming languages and systems, 30 (3): 12, 2008.30 DOI: 10.1145/1353445.1353446. Google ScholarDigital Library
- George C. Necula, Scott McPeak, Shree P. Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction (CC), volume 2304 of LNCS, pages 209--265. Springer, 2002. DOI: 10.1007/3-540-45937-5_16. Google Scholar
- Radu Rugina and Martin Rinard. Symbolic bounds analysis for pointers, array indices, and accessed memory regions. ACM Trans. on Programming Languages and Systems (TOPLAS), 27 (2): 185--235, 2005. DOI: 10.1145/349299.349325. Google ScholarDigital Library
- Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In SAS, number 3148 in LNCS, pages 53--68. Springer, 2004.Google Scholar
- Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Scalable analysis of linear systems using mathematical programming. In VMCAI_2005, pages 21--47. DOI: 10.1007/b105073. Google ScholarCross Ref
- Helmut Seidl, Andrea Flexeder, and Michael Petter. Interprocedurally analysing linear inequality relations. In ESOP_2007, pages 284--299. DOI: 10.1007/978-3-540-71316-6_20. Google Scholar
- Micha Sharir and Amir Pnueli. Two approaches to inter-procedural data-flow analysis. In Program Flow Analysis: Theory and Application. Prentice-Hall, 1981.Google Scholar
- VMCAI05. Verification, Model Checking and Abstract Interpretation (VMCAI), number 3385 in LNCS, 2005. Springer. DOI: 10.1007/b105073.Google Scholar
Index Terms
- Automatic modular abstractions for linear constraints
Recommendations
Automatic modular abstractions for linear constraints
POPL '09We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear ...
Bound Analysis for Whiley Programs
The Whiley compiler can generate naive C code, but the code is inefficient because it uses infinite integers and dynamic array sizes. Our project goal is to build up a compiler that can translate Whiley programs into efficient OpenCL code with fixed-...
Proving Theorems by Program Transformation
To Andrzej Skowron on His 70th BirthdayIn this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming ...
Comments