Construction of verified compiler front-ends with program-checking

DOI10.1007/3-540-46562-6_43MaRDI QIDQ2729963zbMATH OpenFDO

Authors Andreas Heberle, Thilo S. Gaul, Wolfgang Goerigk, Gerhard Goos, Wolf Zimmermann

Publication date 23 October 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46562-6_43

Mathematics Subject Classification ID

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

Recommendations

• Formal verification of a compiler back-end generic checker program
• Correct programs without proof? On checker-based program verification
• scientific article; zbMATH DE number 1374873
• scientific article; zbMATH DE number 1832224
• A Completely Verified Realistic Bootstrap Compiler

Cited in

(5)

• A formally verified compiler back-end
• Formal verification of a compiler back-end generic checker program
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• Verifying an Open Compiler Using Multi-language Semantics
• A Completely Verified Realistic Bootstrap Compiler

This page was built for publication: Construction of verified compiler front-ends with program-checking

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