--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Coq as prover



Hi Jens,

thank you for your answer, ACSL by example is an excellent resource.

> One thing, I learned while working with WP is that not every lemma that cannot be verified at first really needs Coq.
> Sometimes, additional lemmas/assertions help in guiding the automatic provers.
> That being said, Coq is definitely worth learning !

I fully agree with you. My goal is to refine lemmas in such a way that
the automatic provers are sufficient.

My knowledge in Coq is still quite basic, but here my question really
is about how to use Frama-C / Coq in combination. It seems to be in
transition away from the native interface and the examples I found all
use native:coq or even now completely removed options like
`-wp-proof`.

Best regards
Matthias