Kopitiam – a unified IDE for developing formally verified Java programs

TR-2013-167, Authors: Hannes Mehnert and Jesper Bengtson

Kopitiam – a unified IDE for developing formally verified Java programs

Hannes Mehnert
Jesper Bengtson

May 2013

Abstract

We present Kopitiam, an Eclipse plugin for certifying full functional correctness of Java programs using higher-order separation logic. Kopitiam extends the Eclipse Java IDE with an interactive environment for program verification, powered by the general-purpose proof assistant Coq. Moreover, Kopitiam includes a
development environment for Coq theories, where users can define program models, and prove theorems required for the program verification.

Technical report TR-2013-167  in IT University Technical Report Series, May 2013.

Available as PDF