Turning Failure into Proof: The ProB Disprover

Abstract

Initially, the ProB disprover used constraint solving to try and find counterexamples to proof obligations generated from Event-B models. Recently, we made the ProB kernel capable of determining whether a search was exhaustive. Hence, one can now also use it as a prover. It uses a technique which guarantees soundness in the following way: if a solution is found it is guaranteed to be correct; if not, the solver can either return the result “definitely false” if the enumeration was exhaustive, or “unknown” if the enumeration was aborted.

Publication
Poster presented at SAT / SMT Summer School
Date