Trends in Relational Program Verification

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.