cminor

MaRDI QIDQ21718swMATHFDO

Official website http://link.springer.com/chapter/10.1007/978-3-540-74591-4_3

Described by source

• Separation Logic for Small-Step cminor

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