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

As Patrick pointed out, „ACSL by Example“ contains several dozens of lemmas that were proven with Coq.

	https://github.com/fraunhoferfokus/acsl-by-example

They are contained in the file

	https://github.com/fraunhoferfokus/acsl-by-example/blob/master/StandardAlgorithms/wp0.script

However, our PDF does NOT explain how to use, let alone how to learn Coq.

	https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf