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

DOI10.1007/BFB0027453zbMATH Open1293.68013MaRDI QIDQ396975FDOQ396975

Authors: Markus Müller-Olm 

Publication date: 14 August 2014

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

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

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)

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
• Title not available (Why is that?)
• 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)