WP Improvements

> Improvement #1: Tailored WP

Source code of WP // original - tailored

The optimization is located in wpAnnot.ml, starting at line 948, where label assertions are required to be proven independently from each other. This enables proving multiple assertions in a single run where the program semantics is factored out as a separate predicate, independent of the label assertions.

> Improvements #2 and #3 : Robust and Adaptable Multi-Core Assertion Prover

Source code of the Assertion Prover // original - parallelized

When the optimization is on, the assertions to prove are dispatched among monitored processes running each an instance of WP, so that proving is performed in a parallel way.

Back to Home