An operational and axiomatic semantics for non-determinism and sequence points in C
From MaRDI portal
Publication:5408409
DOI10.1145/2535838.2535878zbMath1284.68404OpenAlexW2005574148MaRDI QIDQ5408409
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
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
