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