TU Darmstadt / ULB / TUbiblio

Modular, Correct Compilation with Automatic Soundness Proofs

Steinhöfel, Dominic and Hähnle, Reiner
Margaria, Tiziana and Steffen, Bernhard (eds.) (2018):
Modular, Correct Compilation with Automatic Soundness Proofs.
In: Leveraging Applications of Formal Methods, Verification and Validation. Modeling, Cham, Springer International Publishing, pp. 424-447, DOI: 10.1007/978-3-030-03418-4_25, [Online-Edition: https://doi.org/10.1007/978-3-030-03418-4_25],
[Book Section]

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 and Steffen, Bernhard
Creators: Steinhöfel, Dominic and Hähnle, Reiner
Title: Modular, Correct Compilation with Automatic Soundness Proofs
Language: English
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.

Title of Book: Leveraging Applications of Formal Methods, Verification and Validation. Modeling
Series Name: Lecture Notes in Computer Science
Volume: 11244
Place of Publication: Cham
Publisher: Springer International Publishing
ISBN: 978-3-030-03417-7
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 29 Oct 2018 08:42
DOI: 10.1007/978-3-030-03418-4_25
Official URL: https://doi.org/10.1007/978-3-030-03418-4_25
Related URLs:
Funders: This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.
Export:

Optionen (nur für Redakteure)

View Item View Item