swMATH8230MaRDI QIDQ20240FDOQ20240
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/
Cited In (25)
- \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Common compiler optimisations are invalid in the C11 memory model and what we can do about it
- An operational and axiomatic semantics for non-determinism and sequence points in C
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- cminor
- CompCert
- PLuTo
- Paco
- Rtac
- VeriML
- Mtac: a monad for typed tactic programming in Coq
- The verified CakeML compiler backend
- Pilsner
- CompCertS
- GCminor
- BicolanoMT
- Jinja Threads
- CLDC
- Coinduction All the Way Up
- Trace-relating compiler correctness and secure compilation
- A formal C memory model for separation logic
- CompCertS: a memory-aware verified C compiler using pointer as integer semantics
- Translation validation of coloured Petri net models of programs on integers
- Companions, codensity and causality
This page was built for software: CompCertTSO
