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

DOI10.1145/2535838.2535878zbMATH Open1284.68404OpenAlexW2005574148MaRDI QIDQ5408409FDOQ5408409

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

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

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)

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

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

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