Kopitiam

Kopitiam is an Eclipse plugin for certifying full functional correctness of Java programs using a higher-order separation logic. Kopitiam extends the Java IDE with an interactive environment for program verification, powered by the general-purpose proof assistant Coq.

Kopitiam is developed alongside Coqoon, in which users define program models and prove theorems required for the program verification.

The Java perspective (click to enlarge): Java code interleaved with specifications and proof script using antiquotes. Similar to the Coq perspective, the green background indicates commands processed by Coq. The blue background indicates a verified method. On the right the goal viewer shows the current proof state.

Features

Requirements

• Coq (v8.4 or later)
• Java (Java 6 or later)
• Eclipse (v4.2 or later)

Kopitiam is tested regularly on Windows, Mac OS X and Linux.

Installation

1. Start Eclipse.
2. Select the Help → Install New Software... menu option.
3. Paste the line

   Coqoon - http://www.itu.dk/research/tomeso/coqoon/e42

   into the Work with: text box, and press Enter.
4. Select the Kopitiam → Kopitiam feature, and click Next.
5. Agree to the Kopitiam licence agreement, and click Next.

Development

Source repository

Kopitiam's source code is hosted on GitHub, and can be checked out anonymously using the command

git clone git://github.com/hannesm/Kopitiam.git

Issue tracker

Report bugs, issues and problems using the Kopitiam issue tracker.

Contact

Kopitiam is managed by Jesper Bengtson and developed by Hannes Mehnert and Alexander Faithfull (who also maintains this webpage).