Turning Failure into Proof: Evaluating the ProB Disprover

Abstract

The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of determining whether a search was exhaustive, one can also use the disprover as a prover. In this paper, we compare the ProB Prover with the standard automatic provers for B and Event-B, such as ml, pp and the Rodin SMT plug-in. We demonstrate that ProB is able to deal with classes of proof obligations that are not easily discharged by other provers. As benchmarks we use medium sized specifications such as solu- tions to the ABZ 2014 case study, a CAN bus specification and a railway system.

Type
Publication
In Proceedings 1st International Workshop about Sets and Tools (SETS 2014)
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.