CompCertTSO
From MaRDI portal
Software:20240
No author found.
Related Items (13)
Trace-Relating Compiler Correctness and Secure Compilation ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ CompCertS: a memory-aware verified C compiler using pointer as integer semantics ⋮ A formal C memory model for separation logic ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Companions, Codensity and Causality ⋮ Coinduction All the Way Up ⋮ An operational and axiomatic semantics for non-determinism and sequence points in C ⋮ The verified CakeML compiler backend ⋮ Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology ⋮ Translation validation of coloured Petri net models of programs on integers
This page was built for software: CompCertTSO
