Turning Failure into Proof: Evaluating the ProB Disprover

Download

• Paper

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.

Citation

@InProceedings(disprover_eval,
  Author	= {Sebastian Krings and Jens Bendisposto and Michael Leuschel},
  Title		= {{From Failure to Proof: The ProB Disprover for B and Event-B}},
  Booktitle	= {Proceedings SEFM},
  Year		= 2015,
  Series	= {LNCS},
  Volume	= 9276,
  Publisher	= {Springer}
)