# Difference between revisions of "Disprover"

From Event-B

Jump to navigationJump to searchimported>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. | ||

− | |||

− | |||

== Installation == | == Installation == | ||

Line 13: | Line 11: | ||

== 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]] |

## Revision as of 13:33, 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.

## Installation

The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).