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] proving a contract

Hello,

2012/3/27 Magos?nyi ?rp?d <mag at magwas.rulez.org>:
> Opps, maybe I should not even use that plugin?
> What I am really trying to learn is formal verification of the code,
> in the sense that
> - come up with contracts for code which does not have them
> - ensure that contracts are adhered to throughout the code

In that case you should look at Jessie and WP plugins, as Virgile
suggested. They are both able to prove properties on code within a
Hoare logic framework. Jessie is the old plugin, WP is the newer one.
But they have not exactly the same features, so you might try both.

Best regards,
d.