1 option
Modular Compiler Verification : A Refinement-Algebraic Approach Advocating Stepwise Abstraction / by Markus Müller-Olm.
LIBRA Q341 .P7 2004
Available from offsite location
- Format:
- Book
- Author/Creator:
- Müller-Olm, Markus, author.
- Series:
- Computer Science (Springer-11645)
- Lecture notes in computer science 0302-9743 ; 1283.
- Lecture Notes in Computer Science, 0302-9743 ; 1283
- Language:
- English
- Subjects (All):
- Programming languages (Electronic computers).
- Computer architecture.
- Software engineering.
- Computer logic.
- Computers, Special purpose.
- Programming Languages, Compilers, Interpreters.
- Computer System Implementation.
- Software Engineering.
- Logics and Meanings of Programs.
- Special Purpose and Application-Based Systems.
- Local Subjects:
- Programming Languages, Compilers, Interpreters.
- Computer System Implementation.
- Software Engineering.
- Logics and Meanings of Programs.
- Special Purpose and Application-Based Systems.
- Physical Description:
- 1 online resource (XVI, 260 pages).
- Edition:
- First edition 1997.
- Contained In:
- Springer eBooks
- Place of Publication:
- Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1997.
- System Details:
- text file PDF
- Summary:
- 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.
- 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.
- Other Format:
- Printed edition:
- ISBN:
- 978-3-540-69539-4
- 9783540695394
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.