Trends in Relational Program Verification

Buchkapitel

Autor(en):Bernhard Beckert und Mattias Ulbrich
In:Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday
Verleger:Springer
Jahr:2018
Seiten:41-58
Preprint/PDF:BeckertUlbrich2018.pdf
DOI:10.1007/978-3-319-98047-8_3
Links:

Abstract

Relational program verification refers to the verification of relational properties, which relate different programs, different versions of the same program, or the same program for different inputs. Recently, there is a growing interest in relational properties. One of the main reasons for this trend is that relational properties avoid the bottleneck of having to write complex requirement specifications. Instead, the programs that are compared serve as specification of each other. In this chapter, we give an overview of current trends in relational program verification. We describe the main scenarios where relational program verification is employed to ensure dependability of systems, including regression verification and proving non-interference properties. And we discuss recent trends in how to use deductive verification to prove relational properties.

BibTeX

@InCollection{BeckertUlbrich2018,
  author    = {Bernhard Beckert and Mattias Ulbrich},
  editor    = {Peter M{\"{u}}ller and Ina Schaefer},
  title     = {Trends in Relational Program Verification},
  booktitle = {Principled Software Development: Essays Dedicated to Arnd
               Poetzsch-Heffter on the Occasion of his 60th Birthday},
  pages     = {41--58},
  publisher = {Springer},
  year      = {2018},
  month     = oct,
  isbn      = {978-3-319-98047-8},
  doi       = {10.1007/978-3-319-98047-8\_3},
  abstract  = {Relational program verification refers to the verification
               of relational properties, which relate different programs,
               different versions of the same program, or the same program
               for different inputs. Recently, there is a growing interest
               in relational properties. One of the main reasons for this
               trend is that relational properties avoid the bottleneck of
               having to write complex requirement specifications. Instead,
               the programs that are compared serve as specification of each
               other. In this chapter, we give an overview of current trends
               in relational program verification. We describe the main
               scenarios where relational program verification is employed
               to ensure dependability of systems, including regression
               verification and proving non-interference properties. And we
               discuss recent trends in how to use deductive verification to
               prove relational properties.}
}