--- layout: fc_discuss_archives title: Message 2 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



Hello,

I am looking at the WP plugin to prove lemmas for functions. In the
case that the automatic provers do not manage to prove a PO, how does
one proceed to get a script/.v file to be used in Coq to complete a
proof externally?
It seems that most what I found on this topic uses native Coq which is
deprecated now.
Maybe someone can point me to the current documentation for this. The
WP manual presents tip for proof scripts but that seems to be for the
interactive proof editor of the Frama-C GUI.

Thank you for your help,

Best regards
Matthias