article

The octagon abstract domain

Author:

Antoine MinéAuthors Info & Claims

Higher-Order and Symbolic Computation, Volume 19, Issue 1

Pages 31 - 100

https://doi.org/10.1007/s10990-006-8609-1

Published: 01 March 2006 Publication History

Abstract

This article presents the octagon abstract domain , a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form X Y c where X and Y range among program variables and c is a constant in, or automatically inferred. Abstract elements are represented using modified Difference Bound Matrices and we use a normalization algorithm loosely based on the shortest-path closure to compute canonical representations and construct best-precision abstract transfer functions. We achieve a quadratic memory cost per abstract element and a cubic worst-case time cost per abstract operation, with respect to the number of program variables.

In terms of cost and precision, our domain is in between the well-known fast but imprecise interval domain and the costly polyhedron domain. We show that it is precise enough to treat interesting examples requiring relational invariants, and hence, out of the reach of the interval domain. We also present a packing strategy that allows scaling our domain up to large programs by tuning the amount of relationality. The octagon domain was incorporated into the A STRÉE industrial-strength static analyzer and was key in proving the absence of run-time errors in large critical embedded flight control software for Airbus planes.

References

[1]

1. ACI Sécurité & Informatique. Analyse de PROgrammes Numeériques. http://www.cri.ensmp. fr/apron/]]

[2]

2. Airbus. http://www.airbus.com/]]

[3]

3. Astrée. Analyse Statique de logiciels Temps-RÉel embarqués (static analysis of critical real-time embedded software) analyzer page. http://www.astree.ens.fr/]]

[4]

4. Bagnara, R.: Data-flow analysis for constraint logic-based languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy (1997)]]

[5]

5. Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Universitá di Parma, Italy (2005)]]

[6]

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

Digital Library

[7]

7. Bellman, R.: On a routing problem. In: Quarterly of Applied Mathematics, vol. <b>16</b>, pp. 87-90 (1958)]]

[8]

8. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., A., Miné, Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, LNCS, Springer, pp. 85-108. (2002)]]

Digital Library

[9]

9. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: ACM PLDI'03, vol. 548030, pp. 196-207, ACM Press, (2003)]]

Digital Library

[10]

10. Bourdoncle, F.: Abstract interpretation by dynamic partitioning. Journal of Functional Programming 2(4), 407-423 (1992)]]

[11]

11. Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: ACM PLDI'93, pp. 46-55. ACM Press, (1993)]]

Digital Library

[12]

12. Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: SAS'04, vol. 3148 of LNCS, pp. 312-327. Springer (2004)]]

[13]

13. Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: TACAS' 01, vol. 2031 of LNCS, pp. 67-81 (2001)]]

Digital Library

[14]

14. Cormen, T., Leiserson, C., Rivest, R.: Introduction to Algorithms. The MIT Press (1990)]]

Digital Library

[15]

15. Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design, NATO ASI Series F. IOS Press (1999)]]

[16]

16. Cousot, P.: Verification by abstract interpretation. In: Proc. Int. Symp. on Verification-Theory & Practice--Honoring Zohar Manna's 64th Birthday, vol. 2772, pp. 243-268. Springer (2003)]]

[17]

17. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In ISOP'76, pp. 106-130. Dunod, Paris, France (1976)]]

[18]

18. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPU77, pp. 238-252. ACM Press (1977)]]

Digital Library

[19]

19. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming <b>13</b>(2-3), 103-179 (1992)]]

Digital Library

[20]

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

[21]

21. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In: PLILP'92, LNCS, pp. 269-295. Springer (1992)]]

Digital Library

[22]

22. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL'78, pp. 84-97. ACM Press (1978)]]

Digital Library

[23]

23. Deutsch, A. Interprocedural may-alias analysis for pointers: Beyond k-limiting, In: ACM PLDI'94, pp. 230-241. ACM Press (1994)]]

Digital Library

[24]

24. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proc. International Workshop on Automatic verification Methods for Finite State Systems vol. 407 of LNCS, pp. 197-212, Springer]]

Digital Library

[25]

25. Dor, N., Rodeh, M., Sagiv, M.: Cleanness checking of string manipulations in C programs via integer analysis. In: SAS'01, vol. 2126 of LNCS. Springer (2001)]]

Digital Library

[26]

26. Feret, J.: Abstract interpretation of mobile systems. JLAP (2004)]]

[27]

27. Feret, J.: Static analysis of digital filters. In: ESOP'04, vol. 2986 of LNCS. Springer (2004)]]

[28]

28. Feret, J.: The arithmetic-geometric progression abstract domain. In: VMCAI'05, vol. 3385 of LNCS. Springer (2005)]]

Digital Library

[29]

29. Granger, P.: Static analysis of arithmetical congruences. International Journal of Computer Mathematics, <b>30</b>, 165-190 (1989)]]

[30]

30. Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d'un programme. PhD thesis, Université scientifique et medicale de Grenoble, France (1979)]]

[31]

31. Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: SAS'98, vol. 1503 of LNCS, pp. 200-214 (1998)]]

[32]

32. Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: ACSC'97, vol. 19, pp. 102-111 (1997).]]

[33]

33. Jaffar, J., Maher, M., Stuckey, P., Yap, H.: Beyond finite domains. In: PPCP'94, vol. 874 of LNCS, pp. 86-94. Springer (1994)]]

Digital Library

[34]

34. Jeannet, B.: Partitionnement dynamique dans l'analyse de relations Linéaires et application á la Vérification de programmes synchrones. PhD thesis, Institut National Polytechnique de Grenoble, France (2000)]]

[35]

35. Karr, M.: Affine relationships among variables of a program. Acta Informatica, pp. 133-151 (1976)]]

Digital Library

[36]

36. Larsen, K., Weise, C., Yi, W., Pearson, J.: Clock difference diagrams. Nordic Journal of Computing, <b>6</b>(3), 271-298 (1999)]]

Digital Library

[37]

37. Lions, J.L.: ARIANE 5, flight 501 failure, report by the Inquiry Board (1996)]]

[38]

38. Mauborgne, L.: ASTRIÉE: Verification of absence of run-time error. In: Building the Information Society (18th IFIP World Computer Congress), vol. 156, pp. 385-392. Springer (2004)]]

[39]

39. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In ESOP'05, vol. 3444 of LNCS, pp. 5-20. Springer (2005)]]

Digital Library

[40]

40. Measche, M., Berthomieu, B.: Time Petri-nets for analyzing and verifying time dependent communication protocols. Protocol Specification, Testing and Verification III, pp. 161-172 (1983)]]

[41]

41. Miné, A.: The octagon abstract domain library, http://www.di.ens.fr/mine/oct/]]

[42]

42. Miné, A.: On-line octagon abstract domain sample analyzer. http://cgi.di.ens.fr/cgi-bin/mine/octanalhtml/octanalweb/]]

[43]

43. Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: PADO II, vol. 2053 of LNCS, pp. 155-172. Springer (2001)]]

Digital Library

[44]

44. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, IEEE, pp. 310-319. IEEE CS Press (2001)]]

Digital Library

[45]

45. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: ESOP'04, vol. 2986 of LNCS, pp. 3-17. Springer (2004)]]

[46]

46. Miné, A.: Weakly relational numerical abstract domains. PhD thesis, École Polytechnique, Palaiseau, France (2004). http://www.di.ens.fr/mine/these/]]

[47]

47. MØller, J., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: CSL'99, vol. 1683 of LNCS, pp. 111-125. Springer (1999)]]

Digital Library

[48]

48. Moore, R.E.: Interval Analysis. Prentice Hall (1966)]]

[49]

49. OCaml.: The objective Caml system, http://paulliac.inria.fr/ocaml]]

[50]

50. Rugina, R.: Quantitative shape analysis. In: SAS'04, vol. 3148 of LNCS, pp. 228-245. Springer (2004)]]

[51]

51. Shaham, R., Kolodner, E.K., Sagiv, M.: Automatic removal of array memory leaks in java. In: CC'00, LNCS, pp. 50-66. Springer (2000)]]

Digital Library

[52]

52. Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In: LOPSTR'02, vol. 2664 of LNCS, pp. 71-89. Springer (2002)]]

Digital Library

[53]

53. Venet, A.: Nonuniform alias analysis of recursive data structures and arrays. In: SAS'02, vol. 2477 of LNCS, pp. 36-51. Springer (2002)]]

Digital Library

[54]

54. Yovine, S.: Model-checking timed automata. In: Embedded Systems, vol. 1494 of LNCS. Springer (1998)]]

Digital Library

Cited By

Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
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
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3
Show More Cited By

Index Terms

The octagon abstract domain
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
2. Theory of computation
  1. Logic

Recommendations

Sweeping in Abstract Interpretation

In this paper we present how sweeping line techniques, which are very popular in computational geometry, can be adapted for static analysis of computer software by abstract interpretation. We expose how concept of the sweeping line can be used to ...
SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities

We introduce SubPolyhedra (SubPoly), a new family of numerical abstract domains to infer and propagate linear inequalities. The key insight is that the reduced product of linear equalities and intervals produces powerful yet scalable analyses. Abstract ...
The Octagon Abstract Domain
WCRE '01: Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01)

This article presents a new numerical abstract domain for static analysis by abstract interpretation. It extends our previously proposed DBM-based numerical abstract domain and allows us to represent invariants of the form (\pm x \pm y lleq c), where x ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Higher-Order and Symbolic Computation

Higher-Order and Symbolic Computation Volume 19, Issue 1

March 2006

157 pages

ISSN:1388-3690

Issue’s Table of Contents

Copyright © Copyright © 2006 Springer Science + Business Media, LLC.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 March 2006

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

293
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

Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
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
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3
Seidl HErhard JTilscher SSchwarz M(2024)Non-numerical weakly relational domainsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00755-026:4(479-494)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00755-0
Negrini LArceri VOlivieri LCortesi AFerrara P(2024)Teaching Through Practice: Advanced Static Analysis with LiSAFormal Methods Teaching10.1007/978-3-031-71379-8_3(43-57)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71379-8_3
Luo ZSi X(2024)Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive LearningAI Verification10.1007/978-3-031-65112-0_1(1-28)Online publication date: 22-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65112-0_1
Amat NDal Zilio SLe Botlan D(2024)Project and Conquer: Fast Quantifier Elimination for Checking Petri Net ReachabilityVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_5(101-123)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_5
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
Milanese MMiné A(2024)Generation of Violation Witnesses by Under-Approximating Abstract InterpretationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_3(50-73)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_3
Parolini FMiné A(2024)Sound Abstract Nonexploitability AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_15(314-337)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_15
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