The following pages link to cminor (Q21718):
Displaying 16 items.
- Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Proving correctness of a compiler using step-indexed logical relations (Q1744423) (← links)
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- The Relationship Between Separation Logic and Implicit Dynamic Frames (Q2904617) (← links)
- The Relationship between Separation Logic and Implicit Dynamic Frames (Q3000593) (← links)
- A Machine-Checked Framework for Relational Separation Logic (Q3095237) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- A Formalisation of Smallfoot in HOL (Q3183546) (← links)
- Separation Logic for Non-local Control Flow and Block Scope Variables (Q4910424) (← links)
- A certified framework for compiling and executing garbage-collected languages (Q5176947) (← links)
- An operational and axiomatic semantics for non-determinism and sequence points in C (Q5408409) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- Oracle Semantics for Concurrent Separation Logic (Q5458409) (← links)
- Separation Logic Contracts for a Java-Like Language with Fork/Join (Q5505424) (← links)
