Relational Program Reasoning Using Compiler IR (bibtex)
by Moritz Kiefer, Vladimir Klebanov and Mattias Ulbrich
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.
Reference:
Relational Program Reasoning Using Compiler IR (Moritz Kiefer, Vladimir Klebanov and Mattias Ulbrich), In 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Revised Selected Papers (Sandrine Blazy, Marsha Chechik, eds.), Springer, volume 9971, 2016.
Bibtex Entry:
@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},
  http =         {https://formal.iti.kit.edu/biblio/?lang=en&key=KieferKlebanovUlbrich2016},
  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.  },
  keywords =     {IMPROVE},
}
Powered by bibtexbrowser