--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on August 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[no subject]



	https://softwarefoundations.cis.upenn.edu/lf-current/index.html

Once, you have wrapped your had around this introduction it should be much easier for your to write
your own  proofs for ACSL lemmas.

One thing, I learned while working with WP is that not every lemma that cannot be verified at first really needs Coq.
Sometimes, additional lemmas/assertions help in guiding the automatic provers.
That being said, Coq is definitely worth learning !

Jens