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

DOI10.1145/2535838.2535878MaRDI QIDQ5408409zbMATH OpenOpenAlexFDO

Authors 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

separation logicCoqinteractive theorem provingoperational semanticsC verification

Mathematics Subject Classification ID

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

Recommendations

• Aliasing restrictions of C11 formalized in Coq
• A formal C memory model for separation logic
• scientific article; zbMATH DE number 515739
• Towards verification of C programs: Axiomatic semantics of the C-kernel language
• Towards verification of C programs. C-light language and its formal semantics

Cited in

(8)

• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Semi-automated reasoning about non-determinism in C expressions
• Aliasing restrictions of C11 formalized in Coq
• A concrete memory model for CompCert
• A formal C memory model for separation logic
• 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

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408409)