In 1996, After the crash of the Ariane
5 fligh 501, Alain Deutsch amongst
other researchers from INRIA is in charge of understanding the bug.
He uses a prototype of static analyzer (IABC) of Ada source code based
on abstract
interpretation developed after his PhD and is the first to
demonstrate the effectiveness of static analysis on industrial
size applications as explained in ARIANE 5 - The Software Reliability Verification
Process.
After this demonstration INRIA, CNES and Aerospatiale push toward the
creation of PolySpace Technologies a company in charge of the
industrialization of the prototype analyzer and its commercialization.
The PolySpace Verifier statically detects runtime errors and
non-deterministic constructs in software source code. The PolySpace
tool consists of a familly of four tools targeting different languages: Ada (1999), C (2000), Ada95
and C++ (2003).
PolySpace MISRA:C checker is issued in 2005.