The Coq mailing list

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

> On Jan 4, 2016, at 4:03 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
> 
> 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.

Yes, thanks for reminding that. Somehow I assumed that the correctness of the 
tool’s development (i.e., Frama-C). Since I want to emphasize the use of 
external libs. Consider a deductive verification proof from VST and the proof 
from tools like Why3, Frama-C for a same specification, how we can say that 
these two proofs are the same level of trust? I would like to say if the can 
prove the correctness of the later tools development (including the tool 
itself and the external libs), we can guarantee the same level of trust, 
please correct me if it is not so (As the example of the validator in 
complier validation does so according  the claims in some work of Leroy in 
CompCert project)..

—
Chan