Hyperproperties are properties that relate multiple execution traces of one or more programs. A notable subclass, known as k-safety, is capable of expressing practically important properties like program equivalence and non-interference. Furthermore, hyperproperties beyond k-safety, including generalized non-interference (GNI) and co-termination, have significant applications in security.

Automating verification of hyperproperties is challenging, as it involves finding an appropriate alignment of multiple execution traces for successful verification. Merely reasoning about each program copy’s executions separately, or analyzing states from running multiple copies in lock-step, can sometimes lead to failure. Therefore, it necessitates synthesizing a scheduler that dictates when and which program copies move, to ensure an appropriate alignment of multiple traces. With this alignment, synthesizing relational invariants maintained by the aligned states enables us to prove k-safety. Additionally, verifying GNI and co-termination requires synthesis of Skolem functions and ranking functions, respectively.

In this talk, I will explain and compare two approaches for automating relational verification. The first approach is constraint-based, reducing the synthesis problem into a constraint solving problem within a class that extends Constrained Horn Clauses (CHCs). The second approach is based on proof search within an inductive proof system for a first-order fixpoint logic modulo theories.