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

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

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