WP
- Overview
-
This plug-in allows to prove that ACSL contracts are fulfilled for all possible execution of the code. It is based on weakest-precondition calculus and relies on external automated provers and proof assistants to finally assess the desired properties.
Proving properties by WP is a modular approach, which makes it a strong alternative to consider in replacement of traditional unitary testing.
Maturity: industrialized.
- Quick Start
-
$ frama-c -wp file.c
- Technical Notes
-
WP has an internal prover, Qed, which is also used to simplify the proof obligations before being send to external provers.
Recommended external provers
- Alt-Ergo, Coq (native support)
- Z3, CVC4 and all other provers supported by the Why-3 platform
- User Manual and Tutorial
-
For more details about the WP plug-in, including installation instructions, please consult the WP manual and use the Frama-C mailing lists WP Plug-in Manual
The Fraunhofer Fokus Team provides an extensive corpus of ACSL annotations for typical C programs to be proved by WP. It is available online and a public repository hosts the annotated source examples:
Other previous tutorials on deductive verification of C programs with Frama-C plug-ins Jessie or WP can be helpful as well:
Publications:
- Some publications describing the WP plug-in and its applications are listed on the Frama-C wiki