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.
Kopitiam is tested regularly on Windows, Mac OS X and Linux.
Coqoon - http://www.itu.dk/research/tomeso/coqoon/e42into the Work with: text box, and press Enter.
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
Report bugs, issues and problems using the Kopitiam issue tracker.
Kopitiam is managed by Jesper Bengtson and developed by Hannes Mehnert and Alexander Faithfull (who also maintains this webpage).