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

The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command line may look like:

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:

• ACSL by Example, by Fraunhofer FOKUS;

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.

• Introduction to C program proof with Frama-C and WP, by Allan Blanchard;

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.