package coq-katamaran
Separation logic-based verification of instruction sets
Install
Dune Dependency
Authors
Maintainers
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:KatamaranPublished: 21 Oct 2022
Dependencies (5)
-
coq-stdpp
>= "1.7" & < "1.8~" -
coq-iris
>= "3.6" & < "4.0~" -
coq-equations
>= "1.3" & < "1.4~" -
coq
>= "8.15" & < "8.17~" -
dune
>= "3.3"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page