TU Darmstadt / ULB / TUbiblio

Modular, Correct Compilation with Automatic Soundness Proofs

Steinhöfel, Dominic ; Hähnle, Reiner
Margaria, Tiziana ; Steffen, Bernhard (eds.) :

Modular, Correct Compilation with Automatic Soundness Proofs.
[Online-Edition: https://doi.org/10.1007/978-3-030-03418-4_25]
In: Leveraging Applications of Formal Methods, Verification and Validation. Modeling. Lecture Notes in Computer Science, 11244. Springer International Publishing, Cham , S. 424-447. ISBN 978-3-030-03417-7 ISSN 0302-9743
[Buchkapitel] , (2018)

Offizielle URL: https://doi.org/10.1007/978-3-030-03418-4_25

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
Titel: Modular, Correct Compilation with Automatic Soundness Proofs
Sprache: Englisch
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.

Buchtitel: Leveraging Applications of Formal Methods, Verification and Validation. Modeling
Reihe: Lecture Notes in Computer Science
Band: 11244
Ort: Cham
Verlag: Springer International Publishing
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Software Engineering
Hinterlegungsdatum: 29 Okt 2018 08:42
DOI: 10.1007/978-3-030-03418-4_25
Offizielle URL: https://doi.org/10.1007/978-3-030-03418-4_25
Verwandte URLs:
Sponsoren: This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.
Export:

Optionen (nur für Redakteure)

Eintrag anzeigen Eintrag anzeigen