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. Moreover, Kopitiam includes a feature-complete development environment for Coq theories, where users can define program models, and prove theorems required for the program verification.
We are currently working on the next stable release of Kopitiam, and it will be made available on github by the end of August 2013.