A demonstrably correct compiler
From MaRDI portal
DOI10.1007/BF01211435zbMATH Open0712.68025OpenAlexW1973254452WikidataQ122860301 ScholiaQ122860301MaRDI QIDQ749202FDOQ749202
Authors: D. Kharzeev 
Publication date: 1991
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf01211435
Recommendations
- Toward compiler implementation correctness proofs
- scientific article; zbMATH DE number 578229
- Specification, verification and prototyping of an optimized compiler
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Provably correct code generation: a case study
Theory of compilers and interpreters (68N20) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Grammar Analysis and Parsing by Abstract Interpretation
- Semantics of context-free languages
- Information-flow and data-flow analysis of while-programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Compiler specification and verification
- Title not available (Why is that?)
- Logic programming and compiler writing
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (8)
- On Trojan horses of Thompson-Goerigk-type, their generation, intrusion, detection and prevention
- Provably correct code generation: a case study
- Title not available (Why is that?)
- Deriving correctness properties of compiled code
- Correct hardware synthesis
- Specification, verification and prototyping of an optimized compiler
- A Completely Verified Realistic Bootstrap Compiler
- Calculating correct compilers
This page was built for publication: A demonstrably correct compiler
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q749202)
