Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction

DOI10.1007/BFB0027453MaRDI QIDQ396975zbMATH OpenFDO

Authors Markus Müller-Olm

Publication date 14 August 2014

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

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• An algebraic approach for compiling real-time programs
• A formally verified compiler back-end
• scientific article; zbMATH DE number 702367
• A Completely Verified Realistic Bootstrap Compiler
• Verified Compilation and the B Method: A Proposal and a First Appraisal

Cited in

(10)

• A formally verified compiler back-end
• Verified software units
• Refinement through restraint: bringing down the cost of verification
• An algebraic approach to the design of compilers for object-oriented languages
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• PLC-automata: A new class of implementable real-time automata
• scientific article; zbMATH DE number 1693493 (Why is no real title available?)
• A formal model of real-time program compilation
• A Completely Verified Realistic Bootstrap Compiler
• Algebraic translations, correctness and algebraic compiler construction

This page was built for publication: Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction

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