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.

Publication
In Proceedings 1st International Workshop about Sets and Tools (SETS 2014)
Avatar
Sebastian Krings
Postdoc

My research interests include formal methods, model checking and logic programming.

Related