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.
Initially, the ProB disprover used constraint solving to try and find counterexamples to proof obligations generated from Event-B models.