@InProceedings{KieferKlebanovUlbrich2016,
author = {Moritz Kiefer and Vladimir Klebanov and Mattias Ulbrich},
title = {Relational Program Reasoning Using Compiler {IR}},
booktitle = {8th Working Conference on Verified Software: Theories, Tools, and Experiments
({VSTTE} 2016), Revised Selected Papers},
pages = {149--165},
year = {2016},
doi = {10.1007/978-3-319-48869-1_12},
editor = {Sandrine Blazy and
Marsha Chechik},
series = {Lecture Notes in Computer Science},
volume = {9971},
year = {2016},
month = nov,
publisher = {Springer}
}
Relational Program Reasoning Using Compiler IR
| Author(s): | Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich |
|---|---|
| In: | 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Revised Selected Papers |
| Publisher: | Springer |
| Series: | Lecture Notes in Computer Science |
| Volume: | 9971 |
| Year: | 2016 |
| Pages: | 149-165 |
| Preprint/PDF: | vstte2016.pdf |
| DOI: | 10.1007/978-3-319-48869-1_12 |
Abstract
Relational program reasoning is concerned with formally comparing pairs of executions of programs. Prominent examples of relational reasoning are program equivalence checking (which considers executions from different programs) and detecting illicit information flow (which considers two executions of the same program). The abstract logical foundations of relational reasoning are, in the meantime, sufficiently well understood. In this paper, we address some of the challenges that remain to make the reasoning practicable. Two major ones are dealing with the feature richness of programming languages such as C and with the weakly structured control flow that many real-world programs exhibit. A popular approach to control this complexity is to define the analyses on the level of an intermediate program representation (IR) such as one generated by modern compilers. In this paper we describe the ideas and insights behind IR-based relational verification. We present a program equivalence checker for C programs operating on LLVM IR and demonstrate its effectiveness by automatically verifying equivalence of functions from different implementations of the standard C library.