Difference between revisions of "SMT 1.4 Performance Results"

From Event-B
Jump to navigationJump to search
imported>Nicolas
imported>Nicolas
Line 23: Line 23:
 
The upgraded provers have individually improved their rate of automatically discharged proof obligations.
 
The upgraded provers have individually improved their rate of automatically discharged proof obligations.
  
In particular, veriT has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.
+
In particular, '''veriT''' has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.
  
CVC4 has also greatly improved since its latest release: -22.4% of remaining POs.
+
'''CVC4''' has also greatly improved since its latest release: -22.4% of remaining POs.
  
Z3 has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, z3 remains the SMT prover with the best results.
+
'''Z3''' has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, Z3 remains the SMT prover with the best results.
  
 
Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.
 
Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.

Revision as of 14:57, 11 September 2017

In SMT plug-in 1.4.0, the following bundled provers have been upgraded:

  • veriT (v2012 to v2016)
  • CVC4 (v1.4 to v1.5)
  • Z3 (v4.4.1 to v4.5.0)

Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3.

This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.

The following picture shows the discharged POs for each project of the performance benchmark:

SMT 1.4 Perf Discharged POs.png

This next image focuses on the remaining POs:

SMT 1.4 Perf Remaining POs.png

Now considering the whole benchmark for every prover:

SMT 1.4 Perf Total Remaining POs.png

Conclusion

The upgraded provers have individually improved their rate of automatically discharged proof obligations.

In particular, veriT has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.

CVC4 has also greatly improved since its latest release: -22.4% of remaining POs.

Z3 has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, Z3 remains the SMT prover with the best results.

Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.