--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on April 2011 ---
Dear Frama-C Users, I'm pleased to announce the release of experimental plug-in WP of Frama-C. The WP plug-in implements a weakest precondition calculus for ACSL annotations through C programs. For each code annotation, this technique generates a bundle of proof obligations, ie. mathematical first-order logic formula that can be submit to automated theorem provers like Alt-Ergo or interactive proof assistants like Coq. Other provers are also supported via the Why platform. The WP 0.3 version is a slightly modified version of the one distributed with Frama-C Carbon-beta 2, see Changelog for details. The WP 0.4 version requires Frama-C Carbon-20120201. WP is distributed under LGPL v2.1 (like Frama-C). Enjoy ! ------------------------------------------------------ http://frama-c.com/wp.html http://frama-c.com/download.html