Relational Program Reasoning Using Compiler IR

Reviewed Paper In Proceedings

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.

BibTeX

@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}
}