Formal verification of translation validators
- 7 January 2008
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 43 (1) , 17-27
- https://doi.org/10.1145/1328897.1328444
Abstract
Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of itssemantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The validators are designed for two instruction scheduling optimizations: list scheduling and trace scheduling.This publication has 15 references indexed in Scilit:
- A machine-checked model for a Java-like language, virtual machine, and compilerACM Transactions on Programming Languages and Systems, 2006
- Formal certification of a compiler back-end orPublished by Association for Computing Machinery (ACM) ,2006
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof AssistantPublished by Springer Nature ,2006
- Catching and Identifying Bugs in Register AllocationPublished by Springer Nature ,2006
- Extracting a data flow analyser in constructive logicTheoretical Computer Science, 2005
- Into the Loops: Practical Issues in Translation Validation for Optimizing CompilersElectronic Notes in Theoretical Computer Science, 2005
- TVOC: A Translation Validator for Optimizing CompilersPublished by Springer Nature ,2005
- Compiler verificationACM SIGSOFT Software Engineering Notes, 2003
- Verified bytecode verifiersTheoretical Computer Science, 2003
- The Code Validation Tool (CVT)International Journal on Software Tools for Technology Transfer, 1998