Disprover: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Jens No edit summary |
imported>Jens |
||
| Line 3: | Line 3: | ||
The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples | The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples | ||
or proofs for a given proof obligation. | or proofs for a given proof obligation. | ||
An early version of the ProB Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 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 [http://stups.hhu.de/w/Special:Publication/disprover_eval the paper describing the disprover as a prover] for more details. | |||
== Installation == | == Installation == | ||
Latest revision as of 13:34, 2 May 2016
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/).
