Compiling sandboxes: formally verified software fault isolation

DOI10.1007/978-3-030-17184-1_18MaRDI QIDQ6070795zbMATH OpenOpenAlexFDO

Authors

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17184-1_18

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Modular software fault isolation as abstract interpretation
• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• Compositional CompCert
• Lightweight verification of separate compilation

Cited in

(1)

• Defining and preserving more C behaviors: verified compilation using a concrete memory model

This page was built for publication: Compiling sandboxes: formally verified software fault isolation

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