Abstract
ASTRÉE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical real-time software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.
This work was supported in part by the French exploratory project ASTREÉ of the Réseau National de recherche et d’innovation en Technologies Logicielles (RNTL).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)
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: Proc. ACM SIGPLAN 2003 Conf. PLDI, San Diego, pp. 196–207. ACM Press, New York (2003)
Mauborgne, L.: ASTRÉE: Verification of absence of run-time error. In: Jacquart, P. (ed.) Building the Information Society, pp. 385–392. Kluwer Academic Publishers, Dordrecht (2004)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th ACM POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. of Logic and Comput. 2, 511–547 (1992)
Miné, A.: Weakly Relational Numerical Abstract Domains. Thèse de doctorat en informatique, École polytechnique, Palaiseau, France (2004)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE, IEEE CS Press, Los Alamitos (2001)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Aamodt, T., Chow, P.: Numerical error minimizing floating-point to fixed-point ANSI C compilation. In: 1st Workshop on Media Processors and DSPs, pp. 3–12 (1999)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 2–58. Springer, Heidelberg (2005)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Alt, M.C.F., Martin, F., Wilhelm, R.: Cache behavior prediction by abstract interpretation. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 52–66. Springer, Heidelberg (1996)
Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proc. ACM SIGPLAN 2004 Conf. PLDI, Washington DC, pp. 231–242. ACM Press, New York (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P. et al. (2005). The ASTREÉ Analyzer. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)