CompCertTSO

MaRDI QIDQ20240swMATHFDO

Official website http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/

Described by source

• CompCertTSO

Cited in

(25)

• 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
• Translation validation of coloured Petri net models of programs on integers
• PLuTo
• CompCert
• cminor
• Paco
• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Rtac
• VeriML
• Common compiler optimisations are invalid in the C11 memory model and what we can do about it
• Companions, codensity and causality
• Pilsner
• GCminor
• CompCertS
• Jinja Threads
• BicolanoMT
• CLDC
• Coinduction All the Way Up
• The verified CakeML compiler backend
• Trace-relating compiler correctness and secure compilation
• Mtac: a monad for typed tactic programming in Coq
• An operational and axiomatic semantics for non-determinism and sequence points in C

This page was built for software: CompCertTSO