Steinhöfel, Dominic ; Hähnle, Reiner
eds.: Margaria, Tiziana ; Steffen, Bernhard (2018)
Modular, Correct Compilation with Automatic Soundness Proofs.
In: Leveraging Applications of Formal Methods, Verification and Validation. Modeling
doi: 10.1007/978-3-030-03418-4_25
Book Section, Bibliographie
Abstract
Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.
| Item Type: | Book Section |
|---|---|
| Erschienen: | 2018 |
| Editors: | Margaria, Tiziana ; Steffen, Bernhard |
| Creators: | Steinhöfel, Dominic ; Hähnle, Reiner |
| Type of entry: | Bibliographie |
| Title: | Modular, Correct Compilation with Automatic Soundness Proofs |
| Language: | English |
| Date: | 2018 |
| Place of Publication: | Cham |
| Publisher: | Springer International Publishing |
| Book Title: | Leveraging Applications of Formal Methods, Verification and Validation. Modeling |
| Series: | Lecture Notes in Computer Science |
| Series Volume: | 11244 |
| DOI: | 10.1007/978-3-030-03418-4_25 |
| URL / URN: | https://doi.org/10.1007/978-3-030-03418-4_25 |
| Corresponding Links: | |
| Abstract: | Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR. |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 29 Oct 2018 08:42 |
| Last Modified: | 29 Oct 2018 08:42 |
| PPN: | |
| Funders: | This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project. |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum