Difference between revisions of "Disprover"

From Event-B
Jump to navigationJump to search
imported>Jens
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/).


How to use it, how it works

Disprover Tutorial