A²I: abstract² interpretation

Abstract

The fundamental idea of Abstract² Interpretation (A²I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A²I is generally meant to use abstract interpretation to analyse properties of program analysers. A²I can be either offline or online. Offline A²I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A²I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.

References

1. Samson Abramsky and Achim Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science, Samson Abramsky, Dov M. Gabbay, and Thomas Stephen Edward Maibaum Maibaum (Eds.). Vol. 3: Semantic Structures. Clarendon Press, Oxford, Chapter 1, 1–168.
2. Bowen Alpern and Fred B. Schneider. 1987. Recognizing Safety and Liveness. Distributed Computing 2, 3 (1987), 117–126.
3. Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella. 2005. Precise widening operators for convex polyhedra. Sci. Comput. Program. 58, 1-2 (2005), 28–56.
4. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival. 2015. Static Analysis and Verification of Aerospace Software by Abstract Interpretation. Foundations and Trends in Programming Languages 2, 2-3 (2015), 71–190.
5. Frédéric Besson, Thomas P. Jensen, and Jean-Pierre Talpin. 1999. Polyhedral Analysis for Synchronous Languages. In Proceedings of the 6th International Static Analysis Symposium (SAS’99), LNCS vol. 1694. Springer, 51–68.
6. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’03). ACM, 196–207.
7. François Bourdoncle. 1992. Abstract Interpretation by Dynamic Partitioning. J. Funct. Program. 2, 4 (1992), 407–423.
8. Cristian Cadar and Alastair F. Donaldson. 2016. Analysing the Program Analyser. In Proceedings of the 38th International Conference on Software Engineering Companion (ICSE’16). ACM, 765–768.
9. Patrick Cousot. 1977. 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, Grenoble, France. 15 p.
10. Patrick Cousot. 1999. The Calculational Design of a Generic Abstract Interpreter. In Calculational System Design, Manfred Broy and Ralf Steinbrüggen (Eds.). NATO ASI Series F. IOS Press, Amsterdam.
11. Patrick Cousot. 2015. Abstracting Induction by Extrapolation and Interpolation. In Proceedings 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’15), LNCS Vol. 8931. Springer, 19–42.
12. Patrick Cousot and Radhia Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming. Dunod, Paris, France, 106–130.
13. Patrick Cousot and Radhia Cousot. 1977a. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’77). ACM, 238–252.
14. Patrick Cousot and Radhia Cousot. 1977b. Static determination of dynamic properties of recursive procedures. In IFIP Conf. on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.). North-Holland Pub. Co., 237–277.
15. Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Proceedings of the 6th Annual ACM Symposium on Principles of Programming Languages (POPL’79). ACM, 269–282.
16. Patrick Cousot and Radhia Cousot. 1992. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, invited paper. In Proceedings of the International Workshop Programming Language Implementation and Logic Programming, LNCS Vol. 631 (PLILP’92). Springer, 269–295.
17. Patrick Cousot and Radhia Cousot. 1993. Galois Connection Based Abstract Interpretations for Strictness Analysis (Invited Paper). In Proceedings of the International Conference on Formal Methods in Programming and Their Applications, LNCS Vol. 735. Springer, 98–127.
18. Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’78). ACM, 84–96.
19. Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2014. Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss. ACM Trans. Program. Lang. Syst. 37, 1 (2014), 1:1–1:35.
20. Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. 2015. Analyzing Program Analyses. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL’15). ACM, 261–273.
21. George Grätzer. 2011. Lattice Theory: Foundation. Birkhäuser, Basel.
22. Nicolas Halbwachs. 1979. Détermination automatique de relations linéaires vérifiées par les variables d’un programme (in French). Thèse de 3 ème cycle informatique. Université de Grenoble Alpes, Grenoble, France.
23. Nicolas Halbwachs, David Merchat, and Laure Gonnord. 2006. Some ways to reduce the space dimension in polyhedra computations. Formal Methods in System Design 29, 1 (2006), 79–95.
24. Nicolas Halbwachs, David Merchat, and Catherine Parent-Vigouroux. 2003. Cartesian Factoring of Polyhedra in Linear Relation Analysis. In Proceedings of 10th International Static Analysis Symposium (SAS’03), LNCS Vol. 2694. Springer, 355–365.
25. Nicolas Halbwachs, Yann-Erick Proy, and Patrick Roumanoff. 1997. Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design 11, 2 (01 Aug 1997), 157–185.
26. Chris Hankin and Sebastian Hunt. 1994. Approximate Fixed Points in Abstract Interpretation. Sci. Comput. Program. 22, 3 (1994), 283–306.
27. Kihong Heo, Hakjoo Oh, and Hongseok Yang. 2016. Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis. In Proceedings of 23rd International Static Analysis Symposium (SAS’16), LNCS Vol. 9837. Springer, 237–256.
28. Kihong Heo, Hakjoo Oh, and Kwangkeun Yi. 2017. Selective conjunction of context-sensitivity and octagon domain toward scalable and precise global static analysis. Softw., Pract. Exper. 47, 11 (2017), 1677–1705.
29. Neil D. Jones and Flemming Nielson. 1995. Abstract Interpretation: A Semantics-based Tool for Program Analysis. In Handbook of Logic in Computer Science (Vol. 4), S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum (Eds.). Oxford University Press, Inc., 527–636. http://dl.acm.org/citation.cfm?id=218623.218637
30. Gary A. Kildall. 1973. A Unified Approach to Global Program Optimization. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’73). ACM, 194–206.
31. Woosuk Lee, Wonchan Lee, Dongok Kang, Kihong Heo, Hakjoo Oh, and Kwangkeun Yi. 2017. Sound Non-Statistical Clustering of Static Analysis Alarms. ACM Trans. Program. Lang. Syst. 39, 4 (2017), 16:1–16:35.
32. Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival. 2017. Semantic-directed clumping of disjunctive abstract states. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. ACM, 32–45.
33. Antoine Miné. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation 19, 1 (2006), 31–100.
34. Alan Mycroft. 1982. Abstract interpretation and optimising transformations for applicative programs. Ph.D. Dissertation. University of Edinburgh, UK.
35. Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2016. Selective X-Sensitive Analysis Guided by Impact Pre-Analysis. ACM Trans. Program. Lang. Syst. 38, 2 (2016), 6:1–6:45.
36. Dana S. Scott. 1972. Mathematical concepts in programming language semantics. In AFIPS Spring Joint Computing Conference (AFIPS Conference Proceedings), Vol. 40. AFIPS, 225–234.
37. Gagandeep Singh, Markus Püschel, and Martin Vechev. 2015. Making Numerical Program Analysis Fast. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15). ACM, 303–313.
38. Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (POPL’17). ACM, 46–59.
39. Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2018. A practical construction for decomposing numerical abstract domains. Proc. ACM Program. Lang. 2, POPL (2018), 55:1–55:28.
40. Arnaud Venet. 1996. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Proceedings of the 3rd International Static Analysis Symposium (SAS’96), LNCS Vol. 1145. Springer, 366–382.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Formal language definitions

      • Semantics

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Automated static analysis

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program analysis