The Coq mailing list

[Claude Marché <Claude.Marche AT inria.fr>]

Hello, and Happy New Year to all!

Le 02/01/2016 13:47, Chan Ngo a écrit :
> I have a quick question:
> How do we compare this tool with other deductive verification tools for
> C programs (i.e., Why3, Frama-C)?

Here is a quick answer: Frama-C is a general environment for static
analysis of C source code. Many Frama-C plugins exist, the most popular
one provides a mostly automatic static analysis via abstract
interpretation. See http://frama-c.com/framaCDay.html for recent
non-trivial applications of Frama-C.

There exist two plugins (Jessie and WP) for deductive verification,
aiming at proving that a C code satisfies a user-written formal
specification, written in the dedicated ACSL language. These plugins use
Why3 as a back-end to call external provers, usually automatic ones: SMT
solvers like Z3, CVC4 and Alt-Ergo. Performing a proof via an
interactive proof assistant such as Coq, Isabelle/HOL or PVS is a
possible alternative (for the brave persons only...)

So, in short:

VST: specification language = Coq, back-end prover = Coq
Frama-C/Why3: specification language = ACSL, back-end provers = SMT solvers

VST provides a much higher level of trust than the latter, thanks to the
use of CompCert. There was an attempt to design a Frama-C deductive
verification plugin of Frama-C through CompCert (PhD thesis of Paolo
Hemrs, https://tel.archives-ouvertes.fr/tel-00789543) but it did not
make its way to a robust, distributed plug-in.

A deeper comparison would certainly need a longer answer. I think is it
very good that both approaches exist!

- Claude


-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |