The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 01/04/2016 04:23 AM, Chan Ngo wrote:
> > On Jan 4, 2016, at 9:55 AM, Claude Marché 
> > <Claude.Marche AT inria.fr>
> >  wrote:
> >
> > 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.

I'm afraid that description is rather far from accurate, if by 
"automated provers" you mean "SMT solvers."  Frama-C has much trusted 
code having to do with the C language and associated verification 
methodologies.  All of that code would need to be certified/certifying, 
too, not just the SMT solvers.  Compared to proof witnesses from SMT 
solvers, which are relatively well-understood today, it's not as obvious 
how to use proof-generating translations to handle the semantics of C or 
the application of a verification methodology.