Lightweight verification of separate compilation

DOI10.1145/2837614.2837642MaRDI QIDQ2828254zbMATH OpenOpenAlexWikidataFDO

Authors Jeehoon Kang, Yoonseung Kim, Derek Dreyer, Viktor Vafeiadis, Chung-Kil Hur

Publication date 24 October 2016

Published in Proceedings of the 43rd 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/2837614.2837642

zbMATH Keywords

CompCertcompositional compiler verificationseparate compilation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Compositional CompCert
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Verified Compilation for Shared-Memory C
• A Completely Verified Realistic Bootstrap Compiler
• Certificates and Separation Logic

Cited in

(7)

• scientific article; zbMATH DE number 1852160 (Why is no real title available?)
• The verified CakeML compiler backend
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Trace-relating compiler correctness and secure compilation
• Compiling sandboxes: formally verified software fault isolation
• Verifying peephole rewriting in SSA compiler IRs
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs

This page was built for publication: Lightweight verification of separate compilation

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