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: Patrick.Baudin at cea.fr (BAUDIN Patrick)
- Date: Mon, 17 Aug 2020 09:27:03 +0200
- In-reply-to: <CAGkX0vfzkaCJK5UHhQjUzd5VjqkNHeq53CObeg00ib5ZOWPT6w@mail.gmail.com>
- References: <CAGkX0vfzkaCJK5UHhQjUzd5VjqkNHeq53CObeg00ib5ZOWPT6w@mail.gmail.com>
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>
- Follow-Ups:
- [Frama-c-discuss] Using Coq as prover
- From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
- [Frama-c-discuss] Using Coq as prover
- From: matthias.gudemann at gmail.com (Matthias Güdemann)
- [Frama-c-discuss] Using Coq as prover
- References:
- [Frama-c-discuss] Using Coq as prover
- From: matthias.gudemann at gmail.com (Matthias Güdemann)
- [Frama-c-discuss] Using Coq as prover
- Prev by Date: [Frama-c-discuss] Using Coq as prover
- Next by Date: [Frama-c-discuss] Using Coq as prover
- Previous by thread: [Frama-c-discuss] Using Coq as prover
- Next by thread: [Frama-c-discuss] Using Coq as prover
- Index(es):