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)

Full work available at URL https://doi.org/10.1007/BFB0027453

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

(19)

• Algebraic translations, correctness and algebraic compiler construction
• PLC-automata: A new class of implementable real-time automata
• A formal model of real-time program compilation
• Verified software units
• A formally verified compiler back-end
• scientific article; zbMATH DE number 1693493 (Why is no real title available?)
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Refinement through restraint: bringing down the cost of verification
• scientific article; zbMATH DE number 702367 (Why is no real title available?)
• A Completely Verified Realistic Bootstrap Compiler
• An algebraic approach to the design of compilers for object-oriented languages
• An overview of compositional translations
• Formalizing the Edmonds-Karp Algorithm
• Refinement for Monadic Programs
• ConcurrentHOL
• Dijkstra's Shortest Path Algorithm
• Flow Networks and the Min-Cut-Max-Flow Theorem
• Formalizing Push-Relabel Algorithms
• Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

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)