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.2.0.tar.gz
sha256=032fa4857abacf5ebb3def09fbfdb7bc55cd4a5d9a41ee086ca14d2e39a10bd4

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:2022-07-19 logpath:Katamaran

Published: 21 Oct 2022

Dependencies (5)

  1. coq-stdpp >= "1.7" & < "1.8~"
  2. coq-iris >= "3.6" & < "4.0~"
  3. coq-equations >= "1.3" & < "1.4~"
  4. coq >= "8.15" & < "8.17~"
  5. dune >= "3.3"

Dev Dependencies

None

Used by

None

Conflicts

None