CompCertTSO
From MaRDI portal
Publication:5395719
DOI10.1145/2487241.2487248zbMath1281.68072OpenAlexW2064390891WikidataQ121735218 ScholiaQ121735218MaRDI QIDQ5395719
Viktor Vafeiadis, Peter Sewell, Jaroslav Ševčík, F. Zappa Nardelli, Suresh Jagannathan
Publication date: 17 February 2014
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2487241.2487248
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
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 ⋮ Effective abstractions for verification under relaxed memory models ⋮ The verified CakeML compiler backend ⋮ CompCertTSO ⋮ \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
Uses Software
This page was built for publication: CompCertTSO
