Astrée (static analysis)

Astrée is a static analyzer based on abstract interpretation. It analyzes programs written in the C programming language and outputs an exhaustive list of possible runtime errors and assertion violations.

The tool is tailored towards safety-critical embedded code: source programs are assumed not to contain dynamic allocation (malloc); specific analysis techniques are used for common control theory constructs (filters, rate limiters...) and floating-point numbers.

Astrée was developed in Patrick Cousot's group at École Normale Supérieure, a joint group with CNRS, and is marketed by AbsInt GmbH. It is used in the defense/aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is Airbus.^[1]

Astrée is a commercial product available from AbsInt Angewandte Informatik.

Bibliography

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival. 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, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Volume 2566 of Lecture Notes in Computer Science, pp. 85–108, Springer. doi:10.1007/3-540-36377-7_5
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival, A Static Analyzer for Large Safety-Critical Software., In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196–207, ACM. doi:10.1145/781131.781153
David Delmas and Jean Souyris. Astrée: from Research to Industry., Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22–24 August 2007, LNCS 4634, pp. 437–451
Arnaud J. Venet and Michael R. Lowry. 2010. Static analysis for software assurance: soundness, scalability and adaptiveness. In Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER '10). ACM, New York, NY, USA, 393-396. doi:10.1145/1882362.1882442
Jean-Louis Boulanger. Static Analysis of Software: The Abstract Interpretation. ISBN 978-1-84821-320-3. Wiley.
Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Astrée: Proving the Absence of Runtime Errors. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010.
A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, C. Ferdinand. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France.

References

↑ http://www.lemonde.fr/economie/article/2005/04/26/l-avion-qui-bat-des-ailes-a-federe-de-nombreux-chercheurs_643085_3234.html

External links

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.