Skip to main content
SpringerLink
Log in

Why does Astrée scale up?

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Astrée was the first static analyzer able to prove automatically the total absence of runtime errors of actual industrial programs of hundreds of thousand lines. What makes Astrée such an innovative tool is its scalability, while retaining the required precision, when it is used to analyze a specific class of programs: that of reactive control-command software. In this paper, we discuss the important choice of algorithms and data-structures we made to achieve this goal. However, what really made this task possible was the ability to also take semantic decisions, without compromising soundness, thanks to the abstract interpretation framework. We discuss the way the precision of the semantics was tuned in Astrée in order to scale up, the differences with some more academic approaches and some of the dead-ends we explored. In particular, we show a development process which was not specific to the particular usage Astrée was built for, hoping that it might prove helpful in building other scalable static analyzers.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

References

  1. Bagnara R, Hill PM, Mazzi E, Zaffanella E (2005) Widening operators for weakly-relational numeric abstractions. In: Hankin C, Siveroni I (eds) Proc 12th int symp SAS ’05, London, 7–9 Sep 2005. LNCS, vol 3672. Springer, Berlin, pp 3–18

    Google Scholar 

  2. Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T, Schmidt DA, Sudborough IH (eds) The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D Jones. LNCS, vol 2566. Springer, Berlin, pp 85–108

    Google Scholar 

  3. Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proc ACM SIGPLAN ’2003 conf PLDI, San Diego, 7–14 June 2003. ACM, New York, pp 196–207

    Chapter  Google Scholar 

  4. Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Bjørner D, Broy M, Pottosin IV (eds) Proc FMPA, Akademgorodok, Novosibirsk, 28 June–2 July 1993. LNCS, vol 735. Springer, Berlin, pp 128–141

    Google Scholar 

  5. Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C 35(8)

  6. Burstall RM (1974) Program proving as hand simulation with a little induction. In: Rosenfeld JL (ed) Information Processing 74, Stockholm, Aug 5–10 1974. Proc IFIP congress, vol 74. North-Holland, Amsterdam, pp 308–312

    Google Scholar 

  7. Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Proc 12th int conf CAV ’00, Chicago, 15–19 Jul 2000. LNCS, vol 1855. Springer, Berlin, pp 154–169

    Google Scholar 

  8. Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Proc 10th int conf TACAS ’2004, Barcelona, 29 Mar–2 Apr 2004. LNCS, vol 2988. Springer, Berlin, pp 168–176

    Google Scholar 

  9. Colby C, Lee P (1996) Trace-based program analysis. In: 23rd POPL, St Petersburg Beach, 1996. ACM, New York, pp 195–207

    Google Scholar 

  10. Cousot P (1978) Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, 21 Mar 1978

  11. Cousot P (1981) Semantic foundations of program analysis. In: Muchnick SS, Jones ND (eds) Program flow analysis: theory and applications. Prentice Hall, New York, pp 303–342. Chap 10

    Google Scholar 

  12. Cousot P (1999) The calculational design of a generic abstract interpreter. In: Broy M, Steinbrüggen R (eds) Calculational system design. NATO science series, series F: computer and systems sciences, vol 173. IOS Press, Amsterdam, pp 421–505

    Google Scholar 

  13. Cousot P (2000) Partial completeness of abstract fixpoint checking. In: Choueiry BY, Walsh T (eds) Proc 4th int symp SARA ’2000, Horseshoe Bay, 26–29 Jul 2000. LNAI, vol 1864. Springer, Berlin, pp 1–25

    Google Scholar 

  14. Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Proc 2nd int symp on programming. Dunod, Paris, pp 106–130

    Google Scholar 

  15. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL, Los Angeles, 1977. ACM, New York, pp 238–252

    Google Scholar 

  16. Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: 6th POPL, San Antonio, 1979. ACM, New York, pp 269–282

    Google Scholar 

  17. Cousot P, Cousot R (1982) Induction principles for proving invariance properties of programs. In: Néel D (ed) Tools & notions for program construction. Cambridge University Press, Cambridge, pp 43–119

    Google Scholar 

  18. Cousot P, Cousot R (1992) Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe M, Wirsing M (eds) Proc 4th int symp on PLILP ’92, Leuven, 26–28 Aug 1992. LNCS, vol 631. Springer, Berlin, pp 269–295

    Google Scholar 

  19. Cousot P, Cousot R (1993) “À la Burstall” intermittent assertions induction principles for proving inevitability properties of programs. Theor Comput Sci 120:123–155

    Article  MATH  MathSciNet  Google Scholar 

  20. Cousot P, Cousot R (2002) Modular static program analysis. In: Horspool RN (ed) Proc 11th int conf CC ’2002, Grenoble, 6–14 Apr 2002. LNCS, vol 2304. Springer, Berlin, pp 159–178

    Google Scholar 

  21. Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: 5th POPL, Tucson, 1978. ACM, New York, pp 84–97

    Google Scholar 

  22. Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2005) The Astrée analyser. In: Sagiv M (ed) Proc 14th ESOP ’2005, Edinburg, 2–10 Apr 2005. LNCS, vol 3444. Springer, Berlin, pp 21–30

    Google Scholar 

  23. Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2007) Varieties of static analyzers: A comparison with Astrée. In: Hinchey M, Jifeng H, Sanders J (eds) Proc 1st TASE ’07, Shanghai, 6–8 June 2007. IEEE Comput Soc, Los Alamitos, pp 3–17

    Google Scholar 

  24. Cousot P, Ganty P, Raskin J-F (2007) Fixpoint-guided abstraction refinements. In: Filé G, Riis-Nielson H (eds) Proc 14th int symp SAS ’07, Kongens Lyngby, 22–24 Aug 2007. LNCS, vol 4634. Springer, Berlin, pp 333–348

    Google Scholar 

  25. Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2008) Combination of abstractions in the Astrée static analyzer. In: Okada M, Satoh I (eds) 11th ASIAN 06, Tokyo, 6–8 Dec 2006. LNCS, vol 4435. Springer, Berlin, pp 272–300

    Google Scholar 

  26. Delmas D, Souyris J (2007) Astrée: from research to industry. In: Filé G, Riis-Nielson H (eds) Proc 14th int symp SAS ’07, Kongens Lyngby, 22–24 Aug 2007. LNCS, vol 4634. Springer, Berlin, pp 437–451

    Google Scholar 

  27. D’Silva V, Kroening D, Weissenbacher G (2008) A survey of automated techniques for formal software verification. IEEE Trans Comput-Aided Des Integr Circuits 27(7):1165–1178

    Article  Google Scholar 

  28. Feret J (2004) Static analysis of digital filters. In: Schmidt D (ed) Proc 30th ESOP ’2004, Barcelona, Mar 27–Apr 4, 2004. LNCS, vol 2986. Springer, Berlin, pp 33–48

    Google Scholar 

  29. Feret J (2005) The arithmetic-geometric progression abstract domain. In: Cousot R (ed) Proc 6th int conf VMCAI 2005, Paris, 17–19 Jan 2005. LNCS, vol 3385. Springer, Berlin, pp 42–58

    Google Scholar 

  30. Feret J (2005) Numerical abstract domains for digital filters. In: 1st int work on numerical & symbolic abstract domains, NSAD ’05, Maison Des Polytechniciens, Paris, 21 Jan 2005

  31. Filé G, Ranzato F (1994) Improving abstract interpretations by systematic lifting to the powerset. In: Bruynooghe M (ed) Proc int symp ILPS ’1994, Ithaca, 13–17 Nov 1994. MIT Press, Cambridge, pp 655–669

    Google Scholar 

  32. Floyd RW (1967) Assigning meaning to programs. In: Schwartz JT (ed) Proc symposium in applied mathematics, vol 19. AMS, Providence, pp 19–32

    Google Scholar 

  33. Giacobazzi R, Ranzato F (1998) Optimal domains for disjunctive abstract interpretation. Sci Comput Program 32(1–3):177–210

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  35. Goubault É (2001) Static analyses of floating-point operations. In: Cousot P (ed) Proc 8th int symp SAS ’01, Paris, Jul 2001. LNCS, vol 2126. Springer, Berlin, pp 234–259

    Google Scholar 

  36. Goubault É, Martel M, Putot S (2002) Asserting the precision of floating-point computations: a simple abstract interpreter. In: Le Métayer D (ed) Proc 11th ESOP ’2002, Grenoble, 8–12 Apr 2002. LNCS, vol 2305. Springer, Berlin, pp 209–212

    Google Scholar 

  37. Graf S, Saïdi H (1996) Verifying invariants using theorem proving. In: Alur R, Henzinger TA (eds) Proc 8th int conf CAV ’97, New Brunswick, Jul 31–Aug 3, 1996. LNCS, vol 1102. Springer, Berlin, pp 196–207

    Google Scholar 

  38. Granger P (1989) Static analysis of arithmetical congruences. Int J Comput Math 30(3 & 4):165–190

    Article  MATH  Google Scholar 

  39. Granger P (1991) Improving the results of static analyses of programs by local decreasing iterations. Res rep. LIX/RR/91/08, Laboratoire d’Informatique, École polytechnique, Palaiseau, Dec 1991

  40. Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2008) Automatically refining abstract interpretations. In: Ramakrishnan CR, Rehof J (eds) Proc 14th int conf TACAS ’2000, Budapest, 29 Mar–6 Apr 2008. LNCS, vol 4963. Springer, Berlin, pp 443–458

    Google Scholar 

  41. Handjieva M, Tzolovski S (1998) Refining static analyses by trace-based partitioning using control flow. In: Levi G (ed) Proc 5th int symp SAS ’98, Pisa, 14–16 Sep 1998. LNCS, vol 1503. Springer, Berlin, pp 200–214

    Google Scholar 

  42. Hecht MS (1977) Flow analysis of computer programs. North-Holland/Elsevier, Amsterdam

    MATH  Google Scholar 

  43. Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580

    Article  MATH  Google Scholar 

  44. Jeannet B, Miné A (2007) The Apron numerical abstract domain library. http://apron.cri.ensmp.fr/library/

  45. Lacan P, Monfort JN, Ribal LVQ, Deutsch A, Gonthier G (1998) The software reliability verification process: The Ariane 5 example. In Proceedings DASIA 98—DAta Systems In Aerospace, Athens. ESA Publications, SP-422, 25–28 May 1998

  46. Leroy X, Doligez D, Garrigue J, Rémy D, Vouillon J (2007) The Objective Caml system, documentation and user’s manual (release 3.10). Technical report, INRIA, Rocquencourt, France, 19 May 2007. http://caml.inria.fr/pub/docs/manual-ocaml/

  47. Mauborgne L (2004) Astrée: Verification of absence of run-time error. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 385–392. Chap 4

    Chapter  Google Scholar 

  48. Mauborgne L, Rival X (2005) Trace partitioning in abstract interpretation based static analyzer. In: Sagiv M (ed) Proc 14th ESOP ’2005, Edinburg, Apr 2–10, 2005. LNCS, vol 3444. Springer, Berlin, pp 5–20

    Google Scholar 

  49. Miné A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt D (ed) Proc 30th ESOP ’2004, Barcelona, Mar 27–Apr 4, 2004. LNCS, vol 2986. Springer, Berlin, pp 3–17

    Google Scholar 

  50. Miné A (2004) Weakly relational numerical abstract domains. Thèse de doctorat en informatique, École polytechnique, Palaiseau, 6 Dec 2004

  51. Miné A (2006) Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proc LCTES ’2006. ACM, New York, pp 54–63

    Chapter  Google Scholar 

  52. Miné A (2006) The octagon abstract domain. High-Order Symb Comput 19:31–100

    Article  MATH  Google Scholar 

  53. Miné A (2006) Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson EA, Namjoshi KS (eds) Proc 7th int conf VMCAI 2006, Charleston, 8–10 Jan 2006. LNCS, vol 3855. Springer, Berlin, pp 348–363

    Google Scholar 

  54. Monniaux D (2005) The parallel implementation of the Astrée static analyzer. In: Proc 3rd APLAS ’2005, Tsukuba, 3–5 Nov 2005. LNCS, vol 3780. Springer, Berlin, pp 86–96

    Google Scholar 

  55. Naur P (1966) Proofs of algorithms by general snapshots. BIT 6:310–316

    Article  Google Scholar 

  56. Pioli A, Hind M (1999) Combining interprocedural pointer analysis and conditional constant propagation. Technical Report 99-103, IBM

  57. Randimbivololona F, Souyris J, Deutsch A (2000) Improving avionics software verification cost-effectiveness: Abstract interpretation based technology contribution. In: Proceedings DASIA 2000—DAta Systems In Aerospace, Montreal. ESA Publications, 22–26 May 2000

  58. Rival X, Mauborgne L (2007) The trace partitioning abstract domain. TOPLAS 29(5)

  59. Sagiv M, Reps T, Wilhelm R (1999) Parametric shape analysis via 3-valued logic. In: 26th POPL, San Antonio, 1999. ACM, New York, pp 105–118

    Google Scholar 

  60. Souyris J (2004) Industrial experience of abstract interpretation-based static analyzers. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 393–400. Chap 4

    Chapter  Google Scholar 

  61. Souyris J, Delmas D (2007) Experimental assessment of Astrée on safety-critical avionics software. In: Saglietti F, Oster N (eds) Proc int conf on computer safety, reliability, and security (Safecomp 2007), Nuremberg, 18–21 Sep 2007. LNCS, vol 4680. Springer, Berlin, pp 479–490

    Chapter  Google Scholar 

  62. Su Z, Wagner D (2005) A class of polynomially solvable range constraints for interval analysis without widenings. Theor Comput Sci 345(1):122–138

    Article  MATH  MathSciNet  Google Scholar 

  63. Traverse P, Lacaze I, Souyris J (2004) Airbus fly-by-wire—a total approach to dependability. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 191–212, Chap 3

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Normale Supérieure, 45 rue d’Ulm, 75230, Paris Cedex 05, France

    Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné & Xavier Rival

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radhia Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jérôme Feret
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Laurent Mauborgne
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Antoine Miné
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Xavier Rival
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Patrick Cousot.

Additional information

This work was supported by the INRIA project-team Abstraction common to the CNRS and the École Normale Supérieure.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Cousot, P., Cousot, R., Feret, J. et al. Why does Astrée scale up?. Form Methods Syst Des 35, 229–264 (2009). https://doi.org/10.1007/s10703-009-0089-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-009-0089-6

Search

Navigation