MonKeY¶
Unsupported historical content
This Eclipse integration is no longer supported or maintained. It targeted old Eclipse releases (Indigo/Luna era) and old versions of KeY; the update sites may no longer exist. This page is kept for historical reference.
MonKeY provides a batch verification of all proof obligations. This means that the tool lists all proof obligations provided by the source code and allows to prove them in a batch. Statistics such as the used time or the complexity of proofs are also provided.
The following sections illustrate the main features of MonKeY using screenshots. Each section contains numbered screenshots that explain a usage scenario step by step. Clicking on each picture produces a more detailed view. The screenshots may differ from the latest release.
Prerequisites¶
MonKeY is compatible with Eclipse Indigo (3.7) or newer.
Required update-sites and installation instructions are available in the download area.
Verify all proof obligations of a project¶
-
Select project to load.
-
Select main menu item "KeY, Load Project".
-
Select Application "MonKeY".
-
Select "Start selected Proofs" and wait until all proofs are done.
-
Inspect the result.
