A theory of platform-dependent low-level software

DOI10.1145/1328438.1328465MaRDI QIDQ3189840zbMATH OpenOpenAlexFDO

Authors Marius Nita, Dan Grossman, Craig Chambers

Publication date 12 September 2014

Published in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1328438.1328465

zbMATH Keywords

castslow-level softwareportabilitytype safety

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Dependent Types for Low-Level Programming
• Aliasing restrictions of C11 formalized in Coq
• A concrete memory model for CompCert
• Towards verification of C programs. C-light language and its formal semantics
• Formal verification of object layout for C++ multiple inheritance

Cited in

(2)

• Aliasing restrictions of C11 formalized in Coq
• Formal verification of a C-like memory model and its uses for verifying program transformations

Describes a project that uses

Uses Software

• SAFECode

This page was built for publication: A theory of platform-dependent low-level software

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