The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

On 8/28/2014 8:06 PM, Ömer Sinan Ağacan wrote:
> 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.
The Verified Software Toolchain <http://vst.cs.princeton.edu>
is a system for reasoning about C programs, using Separation Logic,
inside Coq.

-- Andrew Appel