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

Hello,

You may have a look to previous related discussions about:

  * deprecated aspect of native coq prover

    Subjet: [Frama-c-discuss] Frama-C native:coq
    Date: Mon, 10 Feb 2020 13:04:18 +0000
    From: Gerlach, Jens <jens.gerlach at fokus.fraunhofer.de>
    To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>

  * how to perform coq proofs

    Subjet: [Frama-c-discuss] ACSL by Example (version 21.1.0)
    Date: Thu, 9 Jul 2020 17:45:53 +0000
    From: Gerlach, Jens <jens.gerlach at fokus.fraunhofer.de>
    To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>

I hope that using the same method as the one used in ASCL by example 
will help you,
Patrick.

Le 16/08/2020 à 23:21, Matthias Güdemann a écrit :
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin, DILS/LSL, Bât. 862,
Point Courrier n° 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200817/259f3539/attachment.html>