Cited in
(23)- A Formalisation of Smallfoot in HOL
- Practical Tactics for Separation Logic
- The relationship between separation logic and implicit dynamic frames
- Separation logic for non-local control flow and block scope variables
- An operational and axiomatic semantics for non-determinism and sequence points in C
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Multimodal Separation Logic for Reasoning About Operational Semantics
- A formally verified compiler back-end
- A machine-checked framework for relational separation logic
- Oracle Semantics for Concurrent Separation Logic
- A certified framework for compiling and executing garbage-collected languages
- VLISP
- CompCert
- UMM
- GCminor
- MLCompCert
- Piton
- Jape
- The relationship between separation logic and implicit dynamic frames
- Proving correctness of a compiler using step-indexed logical relations
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Mechanized semantics for the clight subset of the C language
This page was built for software: cminor
