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

C verificationCoqinteractive theorem provingoperational semanticsseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) 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)

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)

• CompCertS: a memory-aware verified C compiler using pointer as integer 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
• Aliasing restrictions of C11 formalized in Coq
• A concrete memory model for CompCert
• Semi-automated reasoning about non-determinism in C expressions
• The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics

Describes a project that uses

Uses Software

• Isabelle/HOL
• cminor
• CompCertTSO
• CompCert
• 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)