--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on March 2012 ---
[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.