Astrée (static analysis)
Lua error in package.lua at line 80: module 'strict' not found. 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 http://dx.doi.org/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 http://doi.acm.org/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 http://doi.acm.org/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.
