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

Dear Patrick,

thank you for your answer and the pointers.

> 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>

so from this it means that while the native Coq interface is still
supported it would be the "correct" and future proof way to use WP
driver files.
Is there an example for this?

> 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.

ACSL by example seems to be using the native interface for Coq. So for
now that would be the way to do such proofs if necessary?

Best regards
Matthias