AbstractIn recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses ($$\mathrm {CHCs}$$
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.This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called $$\mathrm {pfwCSP}$$
pfwCSP
where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over $$\mathrm {CHCs}$$
CHCs
permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for $$\mathrm {pfwCSP}$$
pfwCSP
based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.
A New Class of Hard Problem Instances for the 0-1 Knapsack Problem
