Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Coq as prover

  • Subject: [Frama-c-discuss] Using Coq as prover
  • From: matthias.gudemann at gmail.com (Matthias Güdemann)
  • Date: Sun, 16 Aug 2020 23:21:33 +0200
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