Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction by Markus Müller-OlmModular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction by Markus Müller-Olm

Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction

byMarkus Müller-Olm

Paperback | August 6, 1997

Pricing and Purchase Info

$116.95

Earn 585 plum® points

Prices and offers may vary in store

Quantity:

In stock online

Ships free on orders over $25

Not available in stores

about

This book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.
Title:Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise AbstractionFormat:PaperbackDimensions:272 pages, 9.25 × 6.1 × 0.01 inPublished:August 6, 1997Publisher:Springer Berlin Heidelberg

The following ISBNs are associated with this title:

ISBN - 10:3540634061

ISBN - 13:9783540634065

Look for similar items by category:

Reviews

Table of Contents

Complete Boolean lattices.- Galois connections.- States, valuation functions and predicates.- The algebra of commands.- Communication and time.- Data refinement.- Transputer base model.- A small hard real-time programming language.- A hierarchy of views.- Compiling-correctness relations.- Translation theorems.- A functional implementation.- Conclusion.