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.
Categories: Other
Tags: specification, coq, proof, separation logic
Additional Details
Eclipse Versions: Mars (4.5), Luna (4.4), Kepler (4.3), Juno (4.2, 3.8), Previous to Juno (<=4.1), Neon (4.6), Oxygen (4.7), Photon (4.8), 2018-09 (4.9)
Platform Support: Windows, Mac, Linux/GTK
Organization Name: IT University of Copenhagen
Development Status: Beta
Date Created: Wednesday, August 15, 2012 - 11:47
License: BSD
Date Updated: Wednesday, December 14, 2022 - 09:48
Submitted by: Hannes Mehnert
| Date | Ranking | Installs | Clickthroughs |
|---|---|---|---|
| December 2025 | 0/0 | 0 | 1 |
| November 2025 | 0/0 | 0 | 15 |
| October 2025 | 0/0 | 0 | 15 |
| September 2025 | 0/0 | 0 | 18 |
| August 2025 | 0/0 | 0 | 11 |
| July 2025 | 0/0 | 0 | 5 |
| June 2025 | 0/0 | 0 | 11 |
| May 2025 | 0/0 | 0 | 9 |
| April 2025 | 0/0 | 0 | 12 |
| March 2025 | 0/0 | 0 | 10 |
| February 2025 | 0/0 | 0 | 15 |
| January 2025 | 0/0 | 0 | 12 |
Marketplace Drag to Install Button
By adding the following code below to your website you will be able to add an install button for Kopitiam.
HTML Code:
Markdown Syntax:
Output:
