×

zbMATH — the first resource for mathematics

The octagon abstract domain. (English) Zbl 1105.68069
Summary: 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 \(\pm\;X \pm Y \leq c\) where \(X\) and \(Y\) range among program variables and \(c\) is a constant in \(\mathbb Z\), \(\mathbb Q\), or \(\mathbb R\) 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 ASTRÉ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.

MSC:
68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
Apron; ASTREE; Octagon
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1. ACI Sécurité & Informatique. Analyse de PROgrammes Numé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) · Zbl 0891.68056
[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) · Zbl 1141.68445
[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)
[7] 7. Bellman, R.: On a routing problem. In: Quarterly of Applied Mathematics, vol. 16, pp. 87–90 (1958) · Zbl 0081.14403
[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) · Zbl 1026.68514
[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) · Zbl 1026.68514
[10] 10. Bourdoncle, F.: Abstract interpretation by dynamic partitioning. Journal of Functional Programming 2(4), 407–423 (1992) · doi:10.1017/S0956796800000496
[11] 11. Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: ACM PLDI’;93, pp. 46–55. ACM Press, (1993)
[12] 12. Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: SAS’;04, vol. 3148 of LNCS, pp. 312–327. Springer (2004) · Zbl 1104.68410
[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) · Zbl 0978.68095
[14] 14. Cormen, T., Leiserson, C., Rivest, R.: Introduction to Algorithms. The MIT Press (1990) · Zbl 1158.68538
[15] 15. Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design, NATO ASI Series F. IOS Press (1999) · Zbl 0945.68032
[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) · Zbl 1274.68180
[17] 17. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In ISOP’;76, pp. 106–130. Dunod, Paris, France (1976) · Zbl 0393.68080
[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 POPL’;77, pp. 238–252. ACM Press (1977)
[19] 19. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2–3), 103–179 (1992) · Zbl 0776.68024 · doi:10.1016/0743-1066(92)90030-7
[20] 20. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992) · Zbl 0783.68073 · doi:10.1093/logcom/2.4.511
[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) · Zbl 0776.68024
[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)
[23] 23. Deutsch, A. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: ACM PLDI’;94, pp. 230–241. ACM Press (1994)
[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
[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) · Zbl 0997.68570
[26] 26. Feret, J.: Abstract interpretation of mobile systems. JLAP (2004) · Zbl 1066.68087
[27] 27. Feret, J.: Static analysis of digital filters. In: ESOP’;04, vol. 2986 of LNCS. Springer (2004) · Zbl 1126.68347
[28] 28. Feret, J.: The arithmetic-geometric progression abstract domain. In: VMCAI’;05, vol. 3385 of LNCS. Springer (2005) · Zbl 1111.68504
[29] 29. Granger, P.: Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30, 165–190 (1989) · Zbl 0679.68022 · doi:10.1080/00207168908803778
[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)
[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) · Zbl 0358.68025
[36] 36. Larsen, K., Weise, C., Yi, W., Pearson, J.: Clock difference diagrams. Nordic Journal of Computing, 6(3), 271–298 (1999) · Zbl 0937.68086
[37] 37. Lions, J.L.: ARIANE 5, flight 501 failure, report by the Inquiry Board (1996)
[38] 38. Mauborgne, L.: ASTRÉ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) · Zbl 1108.68427
[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/ · Zbl 1105.68069
[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) · Zbl 0984.68034
[44] 44. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, IEEE, pp. 310–319. IEEE CS Press (2001)
[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) · Zbl 1126.68353
[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) · Zbl 0944.68040
[48] 48. Moore, R.E.: Interval Analysis. Prentice Hall (1966) · Zbl 0176.13301
[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) · Zbl 1104.68422
[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)
[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) · Zbl 1278.68072
[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) · Zbl 1015.68513
[54] 54. Yovine, S.: Model-checking timed automata. In: Embedded Systems, vol. 1494 of LNCS. Springer (1998)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.