The Coq mailing list

[Chan Ngo <chan.ngo2203 AT gmail.com>]

Thank you for your prompt reply.

> On Jan 4, 2016, at 9:55 AM, Claude Marché 
> <Claude.Marche AT inria.fr>
>  wrote:
> 
> 
> 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.
> 
I think that if we can certify the automated provers used in that tools, we 
can obtain the same formal level of trust as providing by VST. It is the same 
as some additional parts of the CompCert compiler which use translation 
validation approach (produce a validator), meaning that if we certify the 
validator formally then the result validated compiler is the same level of 
trust as the formal verified compiler.

> 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                    |

Chan Ngo
INRIA,
(+33)02 99 84 72 84
chan.ngo AT inria.fr
http://people.rennes.inria.fr/Chan.Ngo