Trends in Relational Program Verification

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