WP

Overview

This plug-in allows proving that ACSL contracts are fulfilled for all possible executions of the code. It is based on weakest-precondition calculus and relies on external automated provers and proof assistants to finalize the assessment of the desired properties.

Proving properties by WP is a modular approach, which makes it a strong alternative to consider in replacement of traditional unit testing.

Quick Start

frama-c -wp file.c

Technical Notes

  • Maturity: industrialized.
  • WP has an internal prover, Qed, which is also used to simplify proof obligations before they are sent to external provers.

Recommended External Provers:

  • Alt-Ergo
  • Coq
  • Z3
  • CVC4

And all other provers supported by the Why3 platform.

Further Reading

For more details about the WP plug-in, including installation instructions, please consult the WP manual.

Besides the manual, the WP plug-in is used in some tutorials:

This tutorial, written by 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.

This tutorial, written by Allan Blanchard, introduces several notions of program proof before describing ACSL and WP, and how to perform proofs using Frama-C.

Dependencies

This plug-in can (optionally) use the results of the RTE plug-in.