Constraint-based Relational Verification

In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (\(\mathrm {CHCs}\)) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-safety such as generalized non-interference and co-termination.