Tutorial Disprover

WARNING

We believe the Disprover to be useful. The disprover plugin is currently still experimental when used as a prover. Please keep in mind, that you might run into some rough edges or even get wrong results (please inform us about any issues). See the paper describing the disprover as a prover for more details.

Introduction

The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given proof obligation.

The 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.

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

: The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers:

How it works

Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model for that formula. If that is possible, this model is a counter example that will be presented back to the user in the proof tree. The disprover also checks if there cannot be a model for the formula. If this is the case it acts like a decision procedure, i.e., absence of a model is a proof for the goal. This is shown in the proof tree as follows:

Unfortunately, sometimes neither a counter example nor a proof can be found.