Astrée (static analysis)
| Original author(s) | Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival |
|---|---|
| Developer(s) | Laboratoire d'Informatique, École normale supérieure (Paris) (LIENS) French Institute for Research in Computer Science and Automation (INRIA, Paris–Rocquencourt) |
| Initial release | 16 December 2002 |
| Stable release | 23.10
/ 2023 |
| Written in | OCaml |
| Operating system | Windows 10, Linux 64-bit, macOS |
| Platform | x86-64; AArch64 (M1, M2, M3) |
| Available in | English |
| Type | static analyzer |
| License | Proprietary |
| Website | www |
Astrée ("Analyseur statique de logiciels temps-réel embarqués"data races, deadlocks, etc. Astrée includes a static taint checker and helps finding cybersecurity vulnerabilities, such as Spectre. It is proprietary software written in the language OCaml.
The tool is tailored toward safety-critical embedded code: specific analysis techniques are used for common
floating-point
numbers.
Concurrent code is analyzed with a sound interleaving semantics that is aware of the concurrent threads of execution, their priorities and synchronization mechanisms. Astrée supports the ARINC 653, OSEK, and AUTOSAR execution models and can be adapted to added operating system (OS) specifications. On multi-core processors, the placement of threads to cores, and the use of mutex locks and spinlocks are analyzed.
Astrée was developed in
CNRS, and is available commercial from AbsInt GmbH. It is used in the defense–aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is Airbus.[2]
See also
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.
- 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.
- 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.
- 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.
- D. Kästner, L. Mauborgne, N. Grafe, C. Ferdinand. Advanced Sound Static Analysis to Detect Safety- and Security-Relevant Programming Defects. 8th International Journal on Advances in Security, ISSN 1942-2636, vol. 11, no. 1 & 2, 149-159, IARIA, 2018.
- D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software. SAE Technical Paper 2019-01-1246, SAE World Congress 2019, Detroit, April 2019.
References
- ^ "Home". astree.ens.fr.
- ^ "L'Avion qui "bat des ailes" a fédéré de nombreux chercheurs". Le Monde.fr. 26 April 2005.
External links
- Official website
- Astrée industrial/sales page
- Safety-critical C code checked by static analysis tool. EDN Europe, 2013.
| |||||||||
| Programming tools | |||||||||
| Theorem provers, proof assistants | |||||||||
| Designers |
|---|
Book 
Category:Family:ML Category:Family:OCaml Category:Software:OCaml