The ASTR ´ EE Analyzer
Patrick M. Cousot, Radhia Cousot, Laurent Mauborgne, David P. Monniaux, Xavier Rival · 2005
ASTRÉE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical realtime software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.