katamaran
katamaran copied to clipboard
katamaran-project
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 funct...
In the codebase we are using two kinds of environments. `Env` carries a piece of data for every element of a context, and `NamedEnv` carries data for every item in...
The heap predicates have a field that indicates which predicates are precise, and for those it splits up the arguments into inputs and outpus. https://github.com/katamaran-project/katamaran/blob/b7d951c28fc8a0ef6297b91b3531df98b7ee52f0/theories/Syntax/Predicates.v#L56-L69 I wonder why we went...
For pattern matching on unions, we have a version that allows to provide a list of alternatives. https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L181-L182 This list is checked to be exhaustive by a type-level computation https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L163-L167...
For the motivation see the explanation in #41. In the relational operator case in the equality check for fomulas, we start by deciding if the argument types are the same...
In our function for testing for equality of two symbolic terms of the same type, https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/Terms.v#L296-L322 we throw exactly that information away in the binary op case and rather implement...
The symbolic executor uses the inductively defined symbolic propositions directly, i.e. we have essentially the two monads `□(A -> 𝕊) -> 𝕊` and `□(A -> SHeap -> 𝕊) -> SHeap...
Both the shallow and the symbolic executors are implemented in a continuation monad with a proposition answer type. Sometimes we break this abstraction. To fix this I propose to define...
The new shallow executor currently residing in `theories/Staging/NewShallow/Executor.v` uses separation logic propositions directly and does away with a shallow representation of heaps. Moreover, the soundness of this executor is proven...
The new shallow executor currently only has weak monotonicity proofs like e.g. https://github.com/katamaran-project/katamaran/blob/1ff10d9e74e66e89ed9f9729dea041f2d488d7dc/theories/Staging/NewShallow/Executor.v#L917-L922 This monotonicity property is not strong enough to finish the soundness proof of the new shallow executor....
The following snippet ``` From Katamaran Require Import Context. Import ctx ctx.notations. Inductive dom (w : Ctx nat) : Prop := dom_intro : (forall α (αIn : α ∈ w),...
Metadata
Owner
Metadata
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 funct...