NB (update from 2015) These ideas are now improved by our most recent works on refinement for certifying static analyzers.
A static analyzer such as Astrée
is able to ensure safety of critical software, i.e. the
absence of runtime overflows.
But Astrée is itself a very complex software and its full formal verification seems currently impossible.
A more feasible alternative might be to make the analyzer produce a formally verifiable certificate.
Such a certificate would summarize the proof of safety found by the analyzer.
Scat is a tiny Coq-experiment in designing such a certificate language.
Roughly, a Scat certificate annotates the source with loop invariants that are hard to re-infer and also with code transformations used during the analysis.
These code transformations come typically from trace-partitioning (loop unrolling, etc) and linearization of arithmetic expressions.
Currently, our Scat library defines the Scat language, and an automatic checker of Scat certificates which is formally verified in Coq.
Our main Coq theorem ensures that if the Scat certificate is accepted by the checker then the original source is safe.
See Scat report (january 2013) for details.
NB (update from 2014) Treatment of "frames" in this work could be simplified by encapsulating them inside the abstract domain
see our certified abstract domain of polyhedra.
Work supported by french ANR Verasco
The best way to enter in Scat sources is first to read the report and in particular its section 5. Then, as suggested in section 5.3, start browsing file Examples.v
Contact Sylvain.Boulme@imag.fr