--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP 0.3 Released



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