Difference between revisions of "Disprover"
From Event-B
Jump to navigationJump to searchimported>Jens |
imported>Jens |
||
| (One intermediate revision by the same user not shown) | |||
| Line 4: | Line 4: | ||
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 == | ||
| Line 13: | Line 16: | ||
== How to use it, how it works == | == How to use it, how it works == | ||
| − | [ | + | [http://www.prob2.de/Tutorial_Disprover Disprover Tutorial] |
| − | |||
| − | |||
| − | |||
[[Category:User documentation]] | [[Category:User documentation]] | ||
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/).
