The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello,

2014-08-29 2:06 GMT+02:00 Ömer Sinan Ağacan 
<omeragacan AT gmail.com>:
> Thanks for the pointers. I just skimmed over them and I guess what I
> imagined was something between Bedrock(happens inside Coq) and
> Frama-C(the programming language is C and not some language specific
> to the verification tool, no extraction). Since we don't have what I
> imagined, I'll start with Frama-C.
>

Just a few precisions here, as Frama-C offers various analyzers which
are not all related to Coq: you'll probably be mainly interested in
the Jessie and WP plugins
(http://frama-c.com/jessie.html and http://frama-c.com/wp.html). Both
perform deductive verification, i.e. generate a set of proof
obligations from a formal specification and the corresponding
implementation of a function, and both support Coq as  a back-end for
discharging these proof obligations. WP is completely integrated in
Frama-C's distribution, while Jessie is available through Why, and
requires Why3 to be installed (WP also needs Why3 if you want to use
other provers than Coq or Alt-Ergo).
You might also be interested by Paolo Herms' PhD
(http://tel.archives-ouvertes.fr/tel-00789543), which can be briefly
summarized as the formalization in Coq of the Jessie+Why toolchain,
based on CompCert for the formalization of C semantics.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile