Plugins

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