Astrée

I am often asked about Astrée. Astrée is a sound static analyzer for automatically proving the absence of runtime errors in safety critical imperative programs based on abstract interpretation. Soundness means that if no alarm is raised statically then the absence of runtime errors has been proved formally (see a video on static analysis by Reinhard Wilhelm).
No other commercial static analyzer is known to be sound (see the NIST report). More details and references on Astrée are given on Wikipedia.
Astrée was originally developed at the école normale supérieure in Paris with the support of CNRS and INRIA in collaboration with Airbus France for applications. It was later licenced by ENS and CNRS to

AbsInt (located in Saarbrücken in Germany, see also the AbsInt You Tube channel)

AbsInt considerably developed both the scope of the Astrée analyzer (to C++, invalid concurrent behaviors, good practice rules, etc.) and its human interface.

Astrée is distributed by

ANTYCIP Technologies in France
Joral Technologies in North-America

Other distributors exist all over the world (contact info@absint.com for information).

Last modified: Saturday, 27-May-2023 20:06:43 EDT