article

Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation

Author:

Antoine MinéAuthors Info & Claims

Foundations and Trends in Programming Languages, Volume 4, Issue 3-4

Pages 120 - 372

https://doi.org/10.1561/2500000034

Published: 05 December 2017 Publication History

Abstract

Born in the late 70s, Abstract Interpretation has proven an effectivemethod to construct static analyzers. It has led to successful programanalysis tools routinely used in avionic, automotive, and space industriesto help ensuring the correctness of mission-critical software.This tutorial presents Abstract Interpretation and its use to createstatic analyzers that infer numeric invariants on programs. We firstpresent the theoretical bases of Abstract Interpretation: how to assigna well-defined formal semantics to programs, construct computable approximationsto derive effective analyzers, and ensure soundness, i.e.,any property derived by the analyzer is true of all actual executions -although some properties may be missed due to approximations, a necessarycompromise to keep the analysis automatic, sound, and terminatingwhen inferring uncomputable properties.We describe the classicnumeric abstractions readily available to an analysis designer: intervals,polyhedra, congruences, octagons, etc., as well as domain combiners:the reduced product and various disjunctive completions. This tutorialfocuses not only on the semantic aspect, but also on the algorithmicone, providing a description of the data-structures and algorithms necessaryto effectively implement all our abstractions. We will encountermany trade-offs between cost on the one hand, and precision and expressivenesson the other hand. Invariant inference is formalized on anidealized, toy-language, manipulating perfect numbers, but the principlesand algorithms we present are effectively used in analyzers for realindustrial programs, although this is out of the scope of this tutorial.This tutorial is intended as an entry course in Abstract Interpretation,after which the reader should be ready to read the researchliterature on current advances in Abstract Interpretation and on thedesign of static analyzers for real languages.

References

[1]

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of Java bytecode. In Proc. of the 16th European Symposium on Programming, LNCS, pages 157-172. Springer, 2007.

Digital Library

[2]

G. Amato and F. Scozzari. The abstract domain of parallelotopes. Electronic Notes in Theoretical Computer Science, 287:17-28, 2012. Proceedings of the Fourth International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2012.

Digital Library

[3]

C. Ancourt, F. Coelho, and F. Irigoin. A modular static analysis approach to affine loop invariants detection. Electronic Notes in Theoretical Computer Science, 267(1):3-16, 2010. Proceeding of the Second International Workshop on Numerical and Symbolic Abstract Domains: NSAD 2010.

Digital Library

[4]

R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of LNCS, pages 213-229. Springer, 2002.

[5]

R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. In Proc. of the 5h Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), volume 2477 of LNCS, pages 135-148. Springer, 2004.

[6]

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1-2):28-56, October 2005a.

Digital Library

[7]

R. Bagnara, E. Rodríguez-Carbonell, and E. Zaffanella. Generation of basic semi-algebraic invariants using convex polyhedra. In Static Analysis: 12th International Symposium, SAS 2005, pages 19-34. Springer, 2005b.

Digital Library

[8]

R. Bagnara, P. M. Hill, and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. In Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008), volume 4905 of LNCS, pages 8-21. Springer, 2008a.

[9]

R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1-2):3-21, 2008b.

Digital Library

[10]

R. Bagnara, P. M. Hill, and E. Zaffanella. Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Formal Methods in System Design, 35(3):279-323, 2009.

Digital Library

[11]

R. Bagnara, P. M. Hill, and E. Zaffanella. Exact join detection for convex polyhedra and other numerical abstractions. Computational Geometry: Theory and Applications, 43(5):453-473, 2010.

Digital Library

[12]

G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In Proc. of the Int. Conf. on Compiler Construction (CC'04), number 2985 in LNCS, pages 5-23. Springer, 2004.

[13]

V. Balasundaram and K. Kennedy. A technique for summarizing data access and its use in parallelism enhancing transformations. In ACM PLDI'89, pages 41-53. ACM Press, 1989.

[14]

F. Banterle and R. Giacobazzi. A fast implementation of the octagon abstract domain on graphics hardware. In Static Analysis: 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007. Proceedings, pages 315-332. Springer, 2007.

[15]

C. Bartzis and T. Bultan. Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci., 14(4):605-624, 2003.

[16]

C. Bartzis and T. Bultan. Widening arithmetic automata. In Computer Aided Verification, 16th International Conference, CAV, volume 3114 of LNCS, pages 321-333. Springer, 2004.

[17]

F. Benhamou, F. Goualard, L. Granvilliers, and J.-F. Puget. Revisiting hull and box consistency. In Proc. of the 16th Int. Conf. on Logic Programming, pages 230-244, 1999.

Digital Library

[18]

F. Benoy, A. King, and F. Mesnard. Computing convex hulls with a linear solver. Theory and Practice of Logic Programming, 5(1-2):259-271, 2005.

Digital Library

[19]

Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Springer, 2004.

Digital Library

[20]

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival. Static analysis and verification of aerospace software by abstract interpretation. In AIAA Infotech@Aerospace, number 2010-3385 in AIAA, pages 1-38. AIAA (American Institute of Aeronautics and Astronautics), April 2010.

[21]

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival. Static analysis and verification of aerospace software by abstract interpretation. Foundations and Trends in Programming Languages (FnTPL), 2(2-3):71-190, 2015.

[22]

G. Birkhoff. Lattice theory. In Colloquium Publications, volume 25. Amer. Math. Soc., 3. edition, 1967.

[23]

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 Proc. of the ACM SIGPLAN Conf. on Programming Languages Design and Implementation (PLDI'03), pages 196-207. ACM, June 2003.

Digital Library

[24]

M. Bouaziz. TreeKs: A functor to make numerical abstract domains scalable. In 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2012), volume 287, pages 41-52. Elsevier, September 2012.

Digital Library

[25]

F. Bourdoncle. Abstract interpretation by dynamic partitioning. J. Funct. Program., 2(4):407-423, 1992.

[26]

F. Bourdoncle. Abstract debugging of higher-order imperative languages. SIGPLAN Not., 28(6):46-55, June 1993a.

Digital Library

[27]

F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In Proc. of the Int. Conf. on Formal Methods in Programming and their Applications (FMPA'93), volume 735 of LNCS, pages 128-141. Springer, June 1993b.

[28]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, 35:677-691, 1986.

Digital Library

[29]

R. M. Burstall. Program proving as hand simulation with a little induction. Information Processing, pages 308-312, 1974.

[30]

L. Chen, A. Miné, and P. Cousot. A sound floating-point polyhedra abstract domain. In Proc. of the Sixth Asian Symp. on Programming Languages and Systems (APLAS'08), volume 5356 of LNCS, pages 3-18. Springer, December 2008.

Digital Library

[31]

L. Chen, A. Miné, J. Wang, and P. Cousot. Linear absolute value relation analysis. In Proc. of the 20th European Symp. on Programming (ESOP'11), volume 6602 of LNCS, pages 156-175. Springer, March 2011.

[32]

N. V. Chernikova. Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Computational Mathematics and Mathematical Physics, 8(6):282-293, 1968.

[33]

C. K. Chiu and J. H. M. Lee. Efficient interval linear equality solving in constraint logic programming. Reliable Computing, 8(2):139-174, April 2002.

[34]

E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 8:244-263, 1986.

Digital Library

[35]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In In Tools and Algorithms for the Construction and Analysis of Systems, pages 168-176. Springer, 2004.

[36]

T. Cormen, C. Leiserson, R. Rivest, and C. Stein. Introduction to Algorithms. The MIT Press, second edition, 2001.

[37]

A. Cortesi and M. Zanioli. Widening and narrowing operators for abstract interpretation. Computer Languages, Systems & Structures, 37(1):24-42, 2011.

Digital Library

[38]

A. Cortesi, G. Filé, F. Ranzato, R. Giacobazzi, and C. Palamidessi. Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst., 19(1):7-47, January 1997.

Digital Library

[39]

A. Cortesi, G. Costantini, and P. Ferrara. A survey on product operators in abstract interpretation. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, pages 325-336, 2013.

[40]

A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. In Computer Aided Verification: 17th International Conference, CAV 2005, pages 462-475. Springer, 2005.

Digital Library

[41]

P. Cousot. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. R.R. 88, Laboratoire IMAG, Université scientifique et médicale de Grenoble, September 1977. 15 p.

[42]

P. Cousot. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, chapter 10, pages 303-342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.

[43]

P. Cousot. Types as abstract interpretations, invited paper. In Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 316-331, Paris, France, January 1997. ACM Press.

[44]

P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, 277(1-2):47-103, 2002.

Digital Library

[45]

P. Cousot. Abstracting induction by extrapolation and interpolation. In Verification, Model Checking, and Abstract Interpretation: 16th International Conference, VMCAI 2015, pages 19-42. Springer, 2015.

[46]

P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. of the 2d Int. Symp. on Programming, pages 106-130. Dunod, Paris, France, 1976.

[47]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM Symp. on Principles of Programming Languages (POPL'77), pages 238-252. ACM, January 1977.

Digital Library

[48]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conf. Rec. of the 6th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL'79), pages 269-282. ACM Press, 1979a.

Digital Library

[49]

P. Cousot and R. Cousot. Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics, 81(1):43-57, 1979b.

[50]

P. Cousot and R. Cousot. Comparing the Galois connection and widening/ narrowing approaches to abstract interpretation, invited paper. In Proc. of the Int. Workshop on Programming Language Implementation and Logic Programming (PLILP'92), volume 631 of LNCS, pages 269-295. Springer, 1992a.

[51]

P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511-547, August 1992b.

[52]

P. Cousot and R. Cousot. "à la Burstall" intermittent assertions induction principles for proving inevitability properties of programs. Theoret. Comput. Sci., 120(1):123-155, 1993.

Digital Library

[53]

P. Cousot and R. Cousot. A gentle introduction to formal verification of computer systems by abstract interpretation. In Logics and Languages for Reliability and Security, NATO Science Series III: Computer and Systems Sciences, pages 1-29. IOS Press, 2010.

[54]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conf. Rec. of the 5th Annual ACM SIGPLAN/SIGACT Symp. on Principles of Programming Languages (POPL'78), pages 84-97. ACM, 1978.

Digital Library

[55]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Combination of abstractions in the Astrée static analyzer. In Proc. of the 11th Annual Asian Computing Science Conf. (ASIAN'06), volume 4435 of LNCS, pages 272-300. Springer, December 2006.

[56]

P. Cousot, R. Cousot, and L. Mauborgne. A scalable segmented decision tree abstract domain. In Pnueli Festschrift, volume 6200 of LNCS, pages 72-95. Springer, 2010.

[57]

R. Cousot. Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980.

[58]

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C: A software analysis perspective. In Proc. of the 10th International Conference on Software Engineering and Formal Methods, SEFM'12, pages 233-247. Springer, 2012.

Digital Library

[59]

E. W. Dijkstra. Guarded commands, non-determinacy and formal derivation of programs. Commun. ACM, 18(8):453-457, 1975.

Digital Library

[60]

N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Static Analysis: 8th International Symposium, SAS 2001 Paris, France, July 16-18, 2001 Proceedings, pages 194-212. Springer, 2001.

[61]

J. Feret. Static analysis of digital filters. In Proc. of the 13th European Symp. on Programming (ESOP'04), volume 2986 of LNCS, pages 33-48. Springer, March 2004.

[62]

J. Feret. The arithmetic-geometric progression abstract domain. In Proc. of the 6th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), volume 3385 of LNCS, pages 42-58. Springer, January 2005.

Digital Library

[63]

G. Filé and F. Ranzato. The powerset operator on abstract interpretations. Theoretical Computer Science, 222(1):77-111, 1999.

Digital Library

[64]

R. W. Floyd. Assigning meanings to programs. In Proc. of the American Mathematical Society Symposia on Applied Mathematics, volume 19, pages 19-32, Providence, USA, 1967.

[65]

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey. Interval analysis and machine arithmetic: Why signedness ignorance is bliss. ACM Trans. Program. Lang. Syst., 37(1):1:1-1:35, January 2015.

Digital Library

[66]

K. Ghorbal, E. Goubault, and S. Putot. The zonotope abstract domain Taylor1+. In Proc. of the 21st Int. Conf. on Computer Aided Verification (CAV'09), volume 5643 of LNCS, pages 627-633. Springer, June 2009.

Digital Library

[67]

R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Automata, Languages and Programming: 24th International Colloquium, ICALP '97, pages 771-781. Springer, 1997.

[68]

R. Giacobazzi and F. Ranzato. Optimal domains for disjunctive abstract interpretation. Science of Computer Programming, 32(1):177-210, 1998.

Digital Library

[69]

R. Giacobazzi and F. Scozzari. A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst., 20(5):1067-1109, September 1998.

Digital Library

[70]

R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361-416, March 2000.

Digital Library

[71]

P. Granger. Static analysis of arithmetic congruences. Int. Journal of Computer Mathematics, 30:165-199, 1989.

[72]

P. Granger. Static analysis of linear congruence equalities among variables of a program. In Proc. of the Int. Joint Conf. on Theory and Practice of Soft. Development (TAPSOFT'91), volume 493 of LNCS, pages 169-192. Springer, 1991.

[73]

P. Granger. Improving the results of static analyses of programs by local decreasing iterations. In Foundations of Software Technology and Theoretical Computer Science: 12th Conference, pages 68-79. Springer, 1992.

Digital Library

[74]

P. Granger. Static analyses of congruence properties on rational numbers (extended abstract). In Static Analysis: 4th International Symposium, SAS '97, pages 278-292. Springer, 1997.

Digital Library

[75]

N. Halbwachs and J. Henry. When the decreasing sequence fails. In Static Analysis: 19th International Symposium, SAS 2012, pages 198-213. Springer, 2012.

Digital Library

[76]

M. Handjieva and S. Tzolovski. Refining static analyses by trace-based partitioning using control flow. In Static Analysis: 5th International Symposium, SAS'98, pages 200-214. Springer, 1998.

[77]

C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, October 1969.

Digital Library

[78]

ISO/IEC JTC1/SC22/WG14 working group. C standard. Technical Report 1124, ISO & IEC, 2007.

[79]

B. 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.

Digital Library

[80]

B. Jeannet and A. Miné. Apron: A library of numerical abstract domains for static analysis. In Proc. of the 21th Int. Conf. on Computer Aided Verification (CAV'09), volume 5643 of LNCS, pages 661-667. Springer, June 2009.

Digital Library

[81]

G. Kahn. Natural semantics. Technical Report 601, INRIA, 1987.

[82]

M. Karr. Affine relationships among variables of a program. Acta Inf., 6:133-151, 1976.

Digital Library

[83]

G. Kildall. A unified approach to global program optimization. In Proc. of the 1st Annual ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL'73), pages 194-206. ACM, 1973.

Digital Library

[84]

J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, 1976.

Digital Library

[85]

S. C. Kleene. Introduction to metamathematics. Bibliotheca mathematica. North-Holland Pub. Co., 1964.

[86]

S. Lang. Introduction to Linear Algebra. Undergraduate Texts in Mathematics. Springer, 1997.

[87]

H. LeVerge. A note on Chernikova's algorithm. Technical Report 635, IRISA, 1992.

[88]

F. Logozzo and M. Fähndrich. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Science of Computer Programming, 75(9):796-807, 2010.

Digital Library

[89]

A. Maréchal, D. Monniaux, and M. Périn. Scalable minimizing-operators on polyhedra via parametric linear programming. In Static Analysis - 24th International Symposium, pages 212-231, 2017.

[90]

I. Mastroeni. Algebraic power analysis by abstract interpretation. Higher-Order and Symbolic Computation, 17(4):297-345, December 2004.

Digital Library

[91]

L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzer. In Proc. of the 14th European Symp. on Programming (ESOP'05), volume 3444 of LNCS, pages 5-20. Springer, April 2005.

Digital Library

[92]

K. McMillan. Symbolic Model Checking. Kluwer, 1993.

Digital Library

[93]

A. Miné. A new numerical abstract domain based on difference-bound matrices. In Proc. of the Second Symposium on Programs as Data Objects (PADO II), volume 2053 of LNCS, pages 155-172. Springer, May 2001.

[94]

A. Miné. Relational abstract domains for the detection of floating-point runtime errors. In Proc. of the European Symp. on Programming (ESOP'04), volume 2986 of LNCS, pages 3-17. Springer, March 2004.

[95]

A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31-100, 2006a.

Digital Library

[96]

A. Miné. Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In Proc. of the ACM SIGPLAN/ SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES'06), pages 54-63. ACM, June 2006b.

Digital Library

[97]

A. Miné. Abstract domains for bit-level machine integer and floating-point operations. In Proc. of the 4th Int. Workshop on Invariant Generation (WING'12), number HW-MACS-TR-0097 in EPiC Series in Computing, page 16. Computer Science, School of Mathematical and Computer Science, Heriot-Watt University, UK, June 2012.

[98]

R. E. Moore. Interval Analysis. Prentice Hall, Englewood Cliffs N. J., USA, 1966.

[99]

M. Müller-Olm and H. Seidl. Analysis of modular arithmetic. In Proc. of the 14th European Symp. on Prog. (ESOP'05), volume 3444 of LNCS, pages 46-60. Springer, April 2005.

Digital Library

[100]

D. Nguyen Que. Robust and generic abstract domain for static program analysis: The polyhedral case. PhD thesis, École des Mines de Paris, 2010.

[101]

H. Oh, K. Heo, W. Lee, W. Lee, and K. Yi. Design and implementation of sparse global analyses for C-like languages. SIGPLAN Not., 47(6):229-238, June 2012.

Digital Library

[102]

S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Proc. of the 11th Int. Conf. on Automated Deduction (CADE'92), volume 607 of LNAI, pages 748-752. Springer, June 1992.

[103]

G. D. Plotkin. A structural approach to operational semantics, 1981.

[104]

W. Pugh. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Commun. of the ACM, 8:4-13, August 1992.

[105]

H. G. Rice. Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc., 74:358-366, 1953.

[106]

E. Rodríguez-Carbonell and D. Kapur. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming, 64(1):54-75, 2007.

Digital Library

[107]

S. Sankaranarayanan, H. Sipma, and Z. Manna. Scalable analysis of linear systems using mathematical programming. In Proc. of the 6th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), volume 3385 of LNCS, pages 21-47. Springer, 2005.

Digital Library

[108]

D. Schmidt. Abstract interpretation from a topological perspective. In Static Analysis: 16th International Symposium, SAS 2009, pages 293-308. Springer, 2009.

Digital Library

[109]

P. Schrammel and B. Jeannet. Logico-numerical abstract acceleration and application to the verification of data-flow programs. In Static Analysis: 18th International Symposium, SAS 2011, pages 233-248. Springer, 2011.

[110]

A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., 1986.

Digital Library

[111]

D. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Technical Report PRG-6, Oxford U. Computing Lab, 1971.

[112]

Y. Seladji. Finding relevant templates via the principal component analysis. In Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, pages 483-499. Springer, 2017.

[113]

A. Simon and A. King. Analyzing string buffers in C. In Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, AMAST '02, pages 365-379. Springer, 2002.

Digital Library

[114]

A. Simon and A. King. Exploiting sparsity in polyhedral analysis. In Proc. of the 12th Int. Symp. on Static Analysis (SAS'05), volume 3672 of LNCS, pages 336-351. Springer, September 2005.

Digital Library

[115]

A. Simon and A. King. Taming the wrapping of integer arithmetic. In Proc. of the 14th Int. Symp. on Static Analysis (SAS'07), volume 4634 of LNCS, pages 121-136. Springer, August 2007.

[116]

A. Simon, A. King, and J. M. Howe. Two variables per linear inequality as an abstract domain. In Proc. of the 12th Int. Conf. on Logic based program synthesis and transformation (LOPSTR'02), volume 2664 of LNCS, pages 71-89. Springer, 2002.

[117]

G. Singh, M. Püschel, and M. Vechev. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 46-59. ACM, 2017.

Digital Library

[118]

A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-310, 1955.

[119]

A. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, pages 67-69. University Mathematical Laboratory, 1949.

[120]

C. Urban and A. Miné. A decision tree abstract domain for proving conditional termination. In Proc. of the 21st International Static Analysis Symposium (SAS'14), volume 8373 of LNCS, pages 302-318. Springer, September 2014.

[121]

A. Venet. A scalable nonuniform pointer analysis for embedded programs. In Proc. of the Int. Symp. on Static Analysis (SAS'04), number 3148 in LNCS, pages 149-164. Springer, 2004.

Cited By

Lesbre DLemerre M(2024)Compiling with Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36563928:PLDI(368-393)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656392
Smith SZhang R(2024)A Pure Demand Operational Semantics with Applications to Program AnalysisProceedings of the ACM on Programming Languages10.1145/36498528:OOPSLA1(1154-1180)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649852
Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Show More Cited By

Index Terms

Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics

Index terms have been assigned to the content through auto-classification.

Recommendations

Static contract checking with abstract interpretation
FoVeOOS'10: Proceedings of the 2010 international conference on Formal verification of object-oriented software

We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification of Contracts (precondition, postconditions and object invariants).

Clousot checks every method ...
Deriving escape analysis by abstract interpretation

Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java ...
Control-flow analysis of function calls and returns by abstract interpretation

Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Publisher

Now Publishers Inc.

Hanover, MA, United States

Publication History

Published: 05 December 2017

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lesbre DLemerre M(2024)Compiling with Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36563928:PLDI(368-393)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656392
Smith SZhang R(2024)A Pure Demand Operational Semantics with Applications to Program AnalysisProceedings of the ACM on Programming Languages10.1145/36498528:OOPSLA1(1154-1180)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649852
Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Fassina NRanzato FZanella M(2024)Robustness verification of k-nearest neighbors by abstract interpretationKnowledge and Information Systems10.1007/s10115-024-02108-466:8(4825-4859)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10115-024-02108-4
Saan SSchwarz MErhard JSeidl HTilscher SVojdani V(2024)Correctness Witness Validation by Abstract InterpretationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_4(74-97)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_4
Bruni RGiacobazzi RGori RRanzato F(2023)A Correctness and Incorrectness Program LogicJournal of the ACM10.1145/358226770:2(1-45)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582267
Chen LWei DYin BWang J(2023)Static analysis of linear absolute value equalities among variables of a programScience of Computer Programming10.1016/j.scico.2022.102906225:COnline publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1016/j.scico.2022.102906
Henry LJéron TMarkey N(2023)Control strategies for off-line testing of timed systemsFormal Methods in System Design10.1007/s10703-022-00403-w60:2(147-194)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1007/s10703-022-00403-w
Campion MUrban CDalla Preda MGiacobazzi R(2023)A Formal Framework to Measure the Incompleteness of Abstract InterpretationsStatic Analysis10.1007/978-3-031-44245-2_7(114-138)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_7
Dimovski A(2023)Error Invariants for Fault Localization via Abstract InterpretationStatic Analysis10.1007/978-3-031-44245-2_10(190-211)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_10
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents