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
- Subject: [Frama-c-discuss] proving a contract
- From: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 30 Mar 2012 09:41:14 +0200
- In-reply-to: <4F718365.9080005@magwas.rulez.org>
- References: <4F716A54.8000307@magwas.rulez.org> <CABbVA-Csjgd3w7iXLnQr=AFeepg7ynEAJr=Thoz7b961UJz9ug@mail.gmail.com> <4F718365.9080005@magwas.rulez.org>
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.
- References:
- [Frama-c-discuss] proving a contract
- From: mag at magwas.rulez.org (Magosányi Árpád)
- [Frama-c-discuss] proving a contract
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] proving a contract
- From: mag at magwas.rulez.org (Magosányi Árpád)
- [Frama-c-discuss] proving a contract
- Prev by Date: [Frama-c-discuss] Inserting global annotation into the AST
- Previous by thread: [Frama-c-discuss] proving a contract
- Index(es):