Turning Failure into Proof: The ProB Disprover


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.

Poster presented at SAT / SMT Summer School 2014
Sebastian Krings

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