--- layout: plugin title: WP description: Deductive proofs of ACSL contracts. key: main swipper: yes ---
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.
$ frama-c -wp file.c
WP has an internal prover, Qed, which is also used to simplify the proof obligations before being send to external provers.
Recommended external provers
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: