--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Combining Simplify and Coq



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