Disprover
From Event-B
Jump to navigationJump to search
ProB Disprover
The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given proof obligation.
An early version of the ProB Disprover is described in Debugging Event-B Models using the ProB Disprover Plug-in, Ligot, Bendisposto, Leuschel.
Recently, the Disprover has been extended to detect cases in which the search for a counter-example was complete, yet there was no result. In this cases, the absence of a counter-example will be reported as a proof. See the paper describing the disprover as a prover for more details.
Installation
The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).
