--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2010 ---
Hello, > I'm trying to prove some C functions with frama-c. Some of the VCs could be > automatically proved by some ATP (e.g. Simplify), but some can't. For the > remaining VCs, I'd like to use Coq. > I proved the first VCs with Simplify: > frama-c -jessie-analysis -jessie-atp simplify file.c > This gives me an output such as "total: 4, valid: 2, unknown: 2" > > Now for the remaining VCs I planned to prove with Coq, I know I can use: > frama-c -jessie-analysis -jessie-atp coq file.c > This creates a file file.jessie/coq/file_why.v, which I can open with the > coqide, and start filling in the proves. > > My question now is: Is there a way to combine simplify and coq, to get a > file_why.v where some of the proofs are already filled in (those that can be > proved by simplify)? "Filled in" would require automatic provers to generate checkable proof certificates, which they don't with a few exceptions. Indeed sometimes automatic provers have correctness bugs and validate VCs that are later found to be false. "Assumed" is the best you can expect. I do not know how far it will take you, but this announcement on frama-c-discuss was visibly by someone who shared similar objectives to yours: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-May/002054.html Let us know if you find a way to make good use of it. Pascal