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 |
---|---|---|---|
February 2025 | 0/0 | 0 | 6 |
January 2025 | 0/0 | 0 | 12 |
December 2024 | 0/0 | 0 | 5 |
November 2024 | 0/0 | 0 | 7 |
October 2024 | 576/663 | 2 | 4 |
September 2024 | 0/0 | 0 | 9 |
August 2024 | 0/0 | 0 | 20 |
July 2024 | 0/0 | 0 | 11 |
June 2024 | 0/0 | 0 | 10 |
May 2024 | 625/682 | 1 | 8 |
April 2024 | 612/687 | 2 | 9 |
March 2024 | 0/0 | 0 | 4 |