Back to Search
Start Over
Formal verification of translation validators: A case study on instruction scheduling optimizations
- Source :
- 35th ACM Symposium on Principles of Programming Languages (POPL 2008), 35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩, POPL
- Publication Year :
- 2008
- Publisher :
- HAL CCSD, 2008.
-
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.
- Subjects :
- Theoretical computer science
Correctness
Trace scheduling
Computer science
0102 computer and information sciences
02 engineering and technology
Translation (geometry)
Mathematical proof
computer.software_genre
01 natural sciences
Scheduling (computing)
0202 electrical engineering, electronic engineering, information engineering
Formal verification
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Programming language
Instruction scheduling
Translation validation
020207 software engineering
Computer Graphics and Computer-Aided Design
Order (business)
010201 computation theory & mathematics
Proof theory
A priori and a posteriori
Compiler
computer
Software
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Journal :
- 35th ACM Symposium on Principles of Programming Languages (POPL 2008), 35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩, POPL
- Accession number :
- edsair.doi.dedup.....11a8fc2d058bf9c0c59bc7212c16f043
- Full Text :
- https://doi.org/10.1145/1328438.1328444⟩