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

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>