Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
Open Access
- 7 December 2005
- journal article
- Published by Elsevier in Electronic Notes in Theoretical Computer Science
- Vol. 141 (2) , 33-51
- https://doi.org/10.1016/j.entcs.2005.02.042
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Verifix: Konstruktion und Architektur verifizierender Übersetzer (Verifix: Construction and Architecture of Verifying Compilers)it - Information Technology, 2004
- A Completely Verified Realistic Bootstrap CompilerInternational Journal of Foundations of Computer Science, 2003
- Verified bytecode verifiersTheoretical Computer Science, 2003
- Translation validation for an optimizing compilerPublished by Association for Computing Machinery (ACM) ,2000
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Efficiently computing static single assignment form and the control dependence graphACM Transactions on Programming Languages and Systems, 1991
- A mechanically verified language implementationJournal of Automated Reasoning, 1989