The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Dear Coq users,

It is my pleasure to announce the first release of the Verasco static 
analyzer. You can download it from its web page :

http://compcert.inria.fr/verasco/

As said in this web page :

Verasco is a static analyzer for the CompCert subset of ISO C 1999 that 
establishes the absence of run-time errors in analyzed programs. The 
analyzer is based on abstract interpretation and combines several 
abstract domains, non-relational (integer intervals, floating-point 
intervals, integer congruences, points-to properties) and relational 
(integer linear inequalities, symbolic equalities). Verasco enjoys a 
modular structure roughly inspired by that of Astrée.

The major novelty of Verasco, compared with other static analysis tools, 
is that it is entirely specified and proved sound using the Coq proof 
assistant. Verasco's proof guarantees, with mathematical certainty, that 
programs that analyze without alarms are free of run-time errors.

--
JH Jourdan