Content area
Establishing relations between programs arises as a task in various verification contexts such as relating new versions of programs with older versions or proving the correctness of program transformations. Existing tools for relational verification provide a high degree of automation, but at the cost of restricting the class of programs handled. Out of scope, in particular, are programs that act on dynamically allocated mutable state. Auto-active tools such as Dafny and Why3, on the other hand, require more user interaction and support verification of a broad class of programs, including those that act on pointers. However, they don’t provide native facilities for relational verification. In the first part of this thesis, we introduce WhyRel, an auto-active tool for the relational verification of pointer programs, based on relational region logic, that bridges this gap. We evaluate WhyRel through challenging verification case studies including establishing representation independence of ADTs and proving the correctness of program optimizations. Through these, we show that relational properties can be verified effectively in auto-active settings.
In the second part of this thesis, we study the relational Hoare logics (RHLs) that underly tools like WhyRel. For relational reasoning, the key to compositionality is the alignment of computation steps which enables asserting relations between chosen intermediate steps. RHLs provide a considerable number of rules that embody various kinds of alignments, some seemingly more expressive than others. However, a single degenerate alignment rule that reduces relational reasoning to unary reasoning suffices to make a RHL complete. Thus, the usual notion of completeness doesn’t offer a way to distinguish between RHLs or shed light on the rules a relational logic should include. In prior work, we introduced alignment completeness as a more satisfactory measure of RHLs and proved alignment completeness of a few RHL rules with respect to ad hoc forms of alignment. We extend these results and prove alignment completeness for a RHL with respect to a very general class of alignments. Finally, we introduce a new relational program logic for forward simulation properties and prove it is both alignment complete and complete in the usual sense.