--- layout: plugin title: WP description: Deductive proofs of ACSL contracts. key: main swipper: yes ---
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

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: