An operational and axiomatic semantics for non-determinism and sequence points in C

DOI10.1145/2535838.2535878zbMath1284.68404OpenAlexW2005574148MaRDI QIDQ5408409

Robbert Krebbers

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/126245

zbMATH Keywords

operational semanticsseparation logicinteractive theorem provingCoqC verification

Mathematics Subject Classification ID

Related Items (7)

Aliasing Restrictions of C11 Formalized in Coq ⋮ A Concrete Memory Model for CompCert ⋮ CompCertS: a memory-aware verified C compiler using pointer as integer semantics ⋮ The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics ⋮ A formal C memory model for separation logic ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics

Uses Software

• Coq
• Isabelle/HOL
• CompCertTSO
• CompCert
• cminor

This page was built for publication: An operational and axiomatic semantics for non-determinism and sequence points in C