Abstract
Everybody knows about failure problems in software: it is an admitted fact that most large software do contain bugs. The cost of such bugs can be very high for our society and many methods have been proposed to try to reduce these failures. While merely reducing the number of bugs may be economically sound in many areas, in critical software (such as found in power plants or aeronautics), no failure can be accepted.
Work supported in part by the Réseau National de recherche et d’innovation en Technologies Logicielles (RNTL) exploratory 2002 prlject ASTRÉE.
Chapter PDF
Similar content being viewed by others
References
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. (2002). Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In Mogensen, T., Schmidt, D.A., and Sud-borough, I.H., editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to NeilD. Jones, LNCS 2566, pages 85–108. Springer.
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. (2003). A static analyzer for large safety-critical software. In Proceedings of the ACMSIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI’03), pages 196–207, San Diego, California, USA. ACM Press.
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, France.
Cousot, P. and Cousot, R. (1976). Static determination of dynamic properties of programs. In Proc. of the Second Int. Symp. on Programming, pages 106–130. Dunod, Paris, France.
Cousot, P. and Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th ACM POPL, pages 238–252.
Cousot, P. and Cousot, R. (1979). Systematic design of program analysis frameworks. In 6 th ACM POPL, pages 269–282.
Cousot, P. and Halbwachs, N. (1978). Automatic discovery of linear restraints among variables of a program. In 5 th ACM POPL, pages 84–97.
Feret, J. (2004). Static analysis of digital filters. In European Symposium on Programming (ESOP’04), LNCS 2986. Springer.
IEEE Computer Society (1985). IEEE standard for binary floating-point arithmetic.
Miné, A. (2001). The octagon abstract domain. In IEEE AST in WCRE, pages 310–319.
Miné, A. (2004). Relational abstract domains for the detection of floating-point run-time errors. In European Symposium on Programming (ESOP’04), LNCS 2986, pages 3–17. Springer.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this paper
Cite this paper
Mauborgne, L. (2004). AstrÉe: Verification of Absence of Runtime Error. In: Jacquart, R. (eds) Building the Information Society. IFIP International Federation for Information Processing, vol 156. Springer, Boston, MA. https://doi.org/10.1007/978-1-4020-8157-6_30
Download citation
DOI: https://doi.org/10.1007/978-1-4020-8157-6_30
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-8156-9
Online ISBN: 978-1-4020-8157-6
eBook Packages: Springer Book Archive