package coq-katamaran

  1. Overview
  2. No Docs
Separation logic-based verification of instruction sets

Install

Dune Dependency

katamaran-project.github.io Edit opam file Versions (2)

Authors

  1. D
    Dominique Devriese
  2. G
    Georgy Lukyanov
  3. S
    Sander Huyghebaert
  4. S
    Steven Keuchel

Maintainers

  1. S
    Steven Keuchel <steven.keuchel@vub.be>

Sources

v0.1.0.tar.gz
sha256=cb3d1b9121cdff09367d04caf01b595affae4600a10e73d2890c07f4aee3cbbb

Description

Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions. It further comes with a complete model based on the Iris separation logic framework.

Tags

keyword:program verification keyword:separation logic keyword:symbolic execution keyword:instruction sets category:Computer Science/Semantics and Compilation/Semantics data:2021-10-15 logpath:Katamaran

Published: 18 Oct 2021

Dependencies (6)

  1. coq-stdpp >= "1.5" & < "1.6"
  2. coq-iris >= "3.4" & < "3.5"
  3. coq-equations >= "1.2" & < "1.4"
  4. coq-bbv >= "1.2" & < "1.3"
  5. coq >= "8.12" & < "8.15"
  6. dune >= "2.5"

Dev Dependencies

None

Used by

None

Conflicts

None