> 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