Steinhöfel, Dominic ; Hähnle, Reiner
Hrsg.: 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
Buchkapitel, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Buchkapitel |
|---|---|
| Erschienen: | 2018 |
| Herausgeber: | Margaria, Tiziana ; Steffen, Bernhard |
| Autor(en): | Steinhöfel, Dominic ; Hähnle, Reiner |
| Art des Eintrags: | Bibliographie |
| Titel: | Modular, Correct Compilation with Automatic Soundness Proofs |
| Sprache: | Englisch |
| Publikationsjahr: | 2018 |
| Ort: | Cham |
| Verlag: | Springer International Publishing |
| Buchtitel: | Leveraging Applications of Formal Methods, Verification and Validation. Modeling |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 11244 |
| DOI: | 10.1007/978-3-030-03418-4_25 |
| URL / URN: | https://doi.org/10.1007/978-3-030-03418-4_25 |
| Zugehörige Links: | |
| Kurzbeschreibung (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. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 29 Okt 2018 08:42 |
| Letzte Änderung: | 29 Okt 2018 08:42 |
| PPN: | |
| Sponsoren: | 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 |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum