Releases: katamaran-project/katamaran
Releases · katamaran-project/katamaran
CCS 2023 Artifact
This release accompanies our paper submitted to CCS2023, titled: Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts.
We provide a general README.md
for the source code, as well as one aimed at the artifact itself: ARTIFACT.md
.
The source code is included as a zip and we also provide a docker image that has all the dependencies installed and builds the project.
Getting started with the project can be done by downloading katamaran-ccs23-image.tar.gz, the docker image, and loading it into Docker:
docker load < katamaran-ccs23-image.tar.gz
docker run -it --rm katamaran/ccs23
Katamaran 0.2.0
What's Changed
- Now compatible with Coq 8.14 and 8.15.
- Support for application-specific abstract pure predicates and user-defined solvers.
- The LinkedList toy example now comes with a full instantiation of the Iris model.
- New heuristics for consuming exact and precise chunks.
- Inlining up to a bound for functions without contracts.
- Speed and memory improvements.
- New custom bit vector library.
- Computing verification condition statistics and sizes.
- Support multiple sets of contracts for the same functions.
Full Changelog: https://github.com/katamaran-project/katamaran/commits/v0.2.0
First release v0.1.0
Release version 0.1.0