Constraint-based Relational Verification
Hiroshi Unno1,2 , Tachio Terauchi3 , and Eric Koskinen4
1

University of Tsukuba, Ibaraki, Japan
2
RIKEN AIP, Tokyo, Japan
3
Waseda University, Tokyo, Japan
4
Stevens Institute of Technology, New Jersey, USA
Abstract. In recent years they have been numerous works that aim toautomate relational verification. Meanwhile, although Constrained Horn
Clauses (CHCs) empower a wide range of verification techniques andtools, 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 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 CHCs permits arbitrary (i.e., possibly non-Horn) clauses,
well-foundedness constraints, functionality constraints, and is capable ofexpressing 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 byautomatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in thisnew language, we present a constraint solving method for pfwCSP basedon 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 thescope of the previous verification frameworks.

Keywords: relational verification, constraint solving, CEGIS

1Introduction

We describe a novel constraint-based approach to automatically solving a wide
range of relational verification problems including k-safety, co-termination [6,10], termination-sensitive non-interference (TS-NI) [63], and generalized noninterference (GNI) [41] for infinite-state programs.
A key challenge in relational property verification is the discovery of relational invariants which relate the states of multiple program executions. However, whereas most prior approaches must fix the execution schedule5 (e.g., lockstep or sequential) [8, 20, 21, 43, 55, 58], a recent work by Shemer et al. [51] has
5

The notion of schedule is also often called an alignment in literature.

2

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

proposed a method to automatically infer sufficient fair schedulers to prove thegoal relational property. Importantly, the schedulers in their approach can besemantic in which the choice of which program to execute can depend on thestates of the programs as opposed to the classic syntactic schedulers such as
lock-step and sequential that can only depend on the control locations. However, their approach requires the user to provide appropriate atomic predicatesand is not fully automatic. Moreover, they only support k-safety properties. A
recent work has proposed a method for automatically verifying non-hypersafety
relational properties but only for finite state systems [19].
Meanwhile, today’s constraint-based frameworks are also insufficient at automating relational verification. The class of predicate constraints called Constrained Horn Clauses (CHCs) [13] has been widely adopted as a “common intermediate language” for uniformly expressing verification problems for various
programming paradigms, such as functional and object-oriented languages. Example uses of the CHCs framework include safety property verification [29,30,36]
and refinement type inference [33,37,54,57,66]. The separation of constraint generation and solving has facilitated the rapid development of constraint generation
tools such as RCaml [57], SeaHorn [30], and JayHorn [36] as well as efficientconstraint solving tools such as SPACER [38], Eldarica [32], and HoIce [14].
Unfortunately, CHCs lack the ingredients to sufficiently express these relationalverification problems.
In this paper we introduce automated support for relational verification by
generalizing CHCs and introducing a new class of predicate Constraint Satisfaction Problems called pfwCSP. This language allows constraints that arearbitrary (i.e., possibly non-Horn) clauses modulo first-order theories over predicate variables that can be functional predicates, well-founded predicates or ordinary predicates. We then show that, thanks to the enhanced predicate variables, pfwCSP can express non-hypersafety relational properties such as cotermination [11], termination-sensitive non-interference (TS-NI) [63], and generalized non-interference (GNI) [41]. In addition, our approach effectively quantifies over the schedule, expressing arbitrary fair semantic scheduling thanks to
non-Horn clauses and functional predicates (functional predicates are needed toexpress fairness in the presence of non-termination which is needed for properties like co-termination and TS-GNI). The flexibility allows our approach toautomatically discover a fair semantic schedule and verify difficult relational
problem instances that require non-trivial schedules. We prove that our encodings are sound and complete. Expressing relational invariants with such flexible
scheduling is not possible with CHCs. However, pfwCSP retains a key benefit ofCHCs: the idea of separating constraint generation from solving.
We next present a novel constraint solving method for pfwCSP based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, wellfounded, and functional predicates. In our method, ordinary predicates represent relational inductive invariants, well-founded predicates witness synchronous
termination, and functional predicates represent Skolem functions witnessing existential quantifiers that encode angelic non-determinism. These witnesses for a

Constraint-based Relational Verification

3

relational property are often mutually dependent and involve many variables
in a complicated way (see Appendix B, D, and F for examples). The synthesis thus needs to use expressive templates without compromising the efficiency.
Stratified CEGIS combines CEGIS [52] with stratified families of templates [56](i.e., decomposing templates into a series of increasingly expressive templates)to achieve completeness in the sense of [34,56], a theoretical guarantee of convergence, and a faster and stable convergence by avoiding the overfitting problem
of expressive templates to counterexamples [45]. The constraint solving method
naturally generalizes a number of previous techniques developed for CHCs solving and invariant/ranking function synthesis, addressing the challenges due tothe generality of pfwCSP that is essential for relational verification.
We have implemented the above framework and have applied our tool PCSat to a diverse collection of 20 relational verification problems and obtained
promising results. The benchmark problems go beyond the capabilities of theexisting related tools (such as CHCs solvers and program verification tools).
PCSat has solved 15 problems fully automatically by synthesizing complex witnesses for relational properties, and for the 5 problems that could not be solved
fully automatically within the time limit, PCSat was able to solve them semiautomatically provided that a part of an invariant is manually given as a hint.

2

Overview

2.1

Relational verification problems

k-safety Consider the following program taken from [51] that uses a summation
to calculate the square of x, and then doubles it.
doubleSquare(bool h, int x) {int z, y=0;
if (h) { z = 2*x; } else { z = x; }while (z>0) { z--; y = y+x; }if (!h) { y = 2*y; }return y;}This program also takes another input h and, if the value of h is true, calculates
the result differently. The classical relational property termination-insensitive
non-interference (TI-NI) says that, roughly, an observer cannot infer the valueof high security variables (h in this case) by observing the outputs (y). This is a
2-safety property [17, 55]: it relates two executions of the same program. In thisexample, we ask whether two executions that initially agree on x (i.e., x1 = x2 )will agree on the resulting y (i.e., y1 = y2 ). The subscripts in these relations
indicate copies of the program: x1 is variable x in the first copy of the programand x2 is variable x in the second copy. More generally, k-safety means that if
the initial states of a k-tuple of programs satisfy a pre-relation Pre, then when
they all terminate the k-tuple of post states will satisfy post-relation Post.

4

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

The literature proposes many ways to reason about k-safety including methods of reducing a multi-program problem to a single-program problem, suchas through self-composition [8, 55, 58], product programs [7], and their variants [21,47,51,53,59]. Their key challenge is that of scheduling: how to interleave
the programs’ executions so that invariants in the combined program are able
to effectively describe cross-program relationships. Indeed, as proved by [51],verifying this example with the naïve lock-step scheduling is impossible with
only linear arithmetic invariants while linear arithmetic invariants suffice with amore “semantic” scheduling that schedules the copy with h1 = false to iterate
the loop twice per each iteration of the loop in the copy with h2 = true.
In this paper, we will describe a way to pose the scheduling problem as a partof a series of constraints so that the search for an effective scheduler is relegatedto the solver level. In our approach, a k-safety verification problem is encoded asa set of constraints containing (ordinary) predicate variables that represent thescheduler to be discovered and a relational invariant preserved by the scheduler.
Specially, we introduce a predicate variable inv that represents a relational invariant and for each A ⊆ {1, . . . , k}, a predicate variable schA (Ve1 , . . . , Vek ) where
Vei are the variables of the ith program, and add constraints that say that if
the predicate is true, then the programs whose index are in A will step forward
while the rest remain still and also inv is preserved by the step. For soundness,
it is important to constrain the scheduler to be fair, i.e., at least one programthat can progress must be scheduled to progress if there is a program that canprogress. As we shall show in Sec. 4, non-Horn clauses are essential to expressing
the fairness constraint. Roughly, the idea is to use a clause with multiple positive predicate variables (i.e., head disjunction) to say “if the relational invariant
holds, then at least one of the unfinished programs must be scheduled to progress.”
Our approach is similar to and is inspired by the approach of [51] that alsoinfers a fair semantic scheduler. However, their approach requires the user toprovide sufficient atomic predicates manually and is not fully automated. By
contrast, our approach soundly-and-completely encodes the k-safety verification
problem together with scheduler inference as a set of constraints thanks to theexpressiveness of pfwCSP, and automatically solves those constraints by thestratified CEGIS algorithm (cf. Sec. 7 for further comparison).
Co-termination Now consider the following pair of programs.
P1cot : while (x>0) { x = x - y; }P2cot : while (x>0) { x = x - 2 × y; }A (non-safety) relational question is whether these programs P1cot and P2cot agree
on termination [6, 10]. In general they do not: if, for example, P1cot is executedwith x < 0 and P2cot with x > 0 ∧ y = 0, the first will terminate while the second
will diverge. However, under the pre-relation Pre ≡ x1 = x2 ∧ y1 = y2 , they willagree on termination: the first program terminates iff the second one does. The
property falls outside of the k-safety fragment as it cannot be refuted by finite
execution traces. It is worth noting that termination-sensitive non-interferenceConstraint-based Relational Verification

5(TS-NI) is the conjunction of TI-NI and co-termination of two copies of the sametarget program with Pre equating the copies’ low inputs.
Proving co-termination, like k-safety, can be aided by scheduler and we canagain use our constraints over predicate variables. But this is not enough. We
need additional constraints to ensure that whenever one of the two has terminated, the other is also guaranteed to terminate. To address this, we next
introduce well-founded predicate variables. These predicate variables will appear
in our generalized language of constraints as terms of the form wfr(Vei , Vei0 ), where
the relation wfr must be discovered by the constraint solving method. (In Sec. 5
we describe how to achieve this through our stratified CEGIS algorithm.) For
the above example, our stratified CEGIS algorithm and our tool PCSat automatically discovers (1) a schedule where the two programs step together whenx1 > 0 and x2 > 0, (2) a relational invariant that implies that if the first program is terminated, then either the second program is terminated or y2 ≥ 1(and vice-versa), and (3) well-founded relations that (combined with the relational invariant) witness that if the loop has terminated in the second program(x2 ≤ 0) but not in the first (x1 > 0), then a transition in the first is wellfounded (and vice-versa). In Sec. 4, we show how co-termination problems canbe soundly-and-completely encoded in pfwCSP.
Generalized non-interference. Now consider the following program.
gniEx(bool high, int low) {if (high) {int x = *int ; if (x >= low) { return x; } else { while (true) {} }} else {int x = low; while (∗bool ) { x++; } return x;}}

The ∗int (resp. ∗bool ) above indicates an integer (resp. a binary) non-deterministic
choice. Termination-insensitive generalized non-interference (TI-GNI) [41] is anextension of non-interference to non-deterministic programs, and it says that forany two copies of the program with possibly different values for the high security
input (high in this example) and with the same value for the low security input(low in this example), if one copy has a terminating execution that ends insome output (the final value of x in this example), then the other copy has
either a terminating execution ending in the same output or a non-terminating
execution. The termination-sensitive variant (TS-GNI) strengthens the condition
by asserting that if one copy has a terminating execution then the other copy
has a terminating execution that ends in the same output. Both GNI variants
are ∀∃ hyperproperties and fall outside of the k-safety fragment.
Verifying GNI requires handling non-determinism. Note that non-determinism
occurs both demonically (i.e., as ∀) and angelically (i.e., as ∃) in GNI. While
handling demonic non-determinism is straightforward in a constraint-based verification since the term variables are implicitly universally quantified, handlingangelic non-determinism is less straightforward.

6

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
P1

…

Pk

Relational property, k-Safety, Co-Termination, Generalized NI

Encodings for, k-Safety, Co-Termination, Generalized NI(Section 4)

pfw-CSP
Constraint
problems(Section 3)

Solving pfw-CSP
via Stratiﬁed
CEGIS(Section 5)

SAT

UNSAT

Implementation & Evaluation (Section 6)

Fig. 1. Overview of the contributions and how they achieve a constraint-based strategy
for relational verification.

Our approach handles finitary angelic non-determinism like ∗bool by adding
non-Horn clauses with head disjunctions that roughly express the condition “therelational invariant remains true in one of the finitely many next step choices”.
To handle infinitary non-determinism like ∗int , we introduce functional predicate
variables denoted f(Ve , r). In these terms, f is a predicate variable to be discovered but with a new wrinkle: this predicate involves a return value r and theinterpretation of f is a total function over Ve . For this example, we introduce
the term f(Ve , r) where r represents the value chosen non-deterministically at∗int and Ve are program variables and prophecy variables that represent the final
return values of the demonic copy. For this example, PCSat automatically discovers the predicate r = ret1 where ret1 is the prophecy variable for the return
value of the demonic copy. With it, PCSat is able to verify TS-GNI and TI-GNIof this example. We remark that functional predicates are also used to encodescheduler fairness in the presence of non-termination and is needed to ensure
soundness for properties like co-termination and TS-GNI. In Sec. 4.3, we show
how TI-GNI and TS-GNI can be soundly-and-completely encoded in pfwCSP.
2.2

Challenges & Contributions

There are several challenges that we face in supporting relational verification
problems with a constraint-based approach. The subsequent sections of this paper are organized around addressing those challenges as follows:– We first ask how to generalize the constraint language to go beyond CHCs to
express a more general class of relational verification problems. To this end,in Sec. 3, we present a new language called predicated constraint satisfaction
problems (pfwCSP), which incorporate non-Horn clauses, (ordinary) predicate variables, well-founded predicate variables, and functional predicate
variables.
– We next return to the above relational verification problems –k-safety, cotermination, and generalized non-interference– and describe how pfwCSP
can express each of them in a sound and complete manner in Sec. 4.
– The next major contribution of our research is a novel stratified CEGIS algorithm for solving pfwCSP constraints. Our approach integrates advanced
verification techniques: stratified family of templates [56] and CEGIS of invariants/ranking functions [14, 26, 28, 46]. While the individual ideas haveConstraint-based Relational Verification

7

been proposed previously, they have only been designed for less expressiveframeworks such as CHCs, and substantial extensions are needed to combine
and apply them to the new pfwCSP framework as we shall show in Sec. 5.
– We next turn to an implementation and experimental validation on a diverse
collection of 20 relational verification problems, consisting of k-safety problems from Shemer et al. [51] and new co-termination and GNI problems in
Sec. 6. As far as we know, none of the existing automated tools other thanour new tool called PCSat can solve them.
In sum, Fig. 1 depicts each of these sections and how, together, they enable
relational verification. For space, the proofs of the soundness and completenesstheorems are deferred to the appendix.

3

Predicate Constraint Satisfaction Problems pfwCSP

As discussed in Sec. 2, CHCs are insufficient to express important relationalverification problems. In the section we introduced a generalized language of
constraints called pfwCSP. The language of constraint satisfaction problems(CSP) permits non-Horn clauses, predicate variable terms, including those forfunctional predicates and well-founded relations (pfw). We now define pfwCSP.
Let T be a (possibly many-sorted) first-order theory with the signature Σ.
The syntax of T -formulas and T -terms is:(formulas) φ ::= X(et) | p(et) | ¬φ | φ1 ∨ φ2 | φ1 ∧ φ2(terms) t ::= x | f (et)
Here, the meta-variables x and X respectively range over term and predicate
variables. The meta-variables p and f respectively denote predicate and function
symbols of Σ. We use s as a meta-variable ranging over sorts of the signature
Σ. We write ? for the sort of propositions and s1 → s2 for the sort of functions
from s1 to s2 . We write ar(o) and sort(o) respectively for the arity and thesort of a syntactic element o. A function f represents a constant if ar(f ) = 0.
We write ftv (φ) and fpv (φ) respectively for the set of free term and predicate
variables that occur in φ. We write xe for a sequence of term variables, |ex| forthe length of xe, and  for the empty sequence. We often abbreviate ¬φ1 ∨ φ2 as
φ1 ⇒ φ2 . We henceforth consider only well-sorted formulas and terms. We use
ϕ as a meta-variable ranging over T -formulas without predicate variables.
We now define a pCSP C (with ordinary but without well-founded and functional predicate variables) to be a finite set of clauses of the form
W


Wm
`
e
e
ϕ∨
X
(
t
)
∨
(1)
i
i
i=1
i=`+1 ¬Xi (ti )where 0 ≤ ` ≤ m. We write ftv (c) for the set of free term variables
S of a clausec. The set of free term variables of C is defined by ftv (C) = c∈C ftv (c). We
regard the variables in ftv (c) as implicitly universally quantified. We write fpv (C)8Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

for the set of free predicate variables that occur in C. A predicate substitution
σ is a finite map from predicate variables X to closed predicates of the form
λx1 , . . . , xar(X) .ϕ. We write σ(C) for the application of σ to C and dom(σ) for
theVdomain of σ. We call σ a syntactic solution for C if fpv (C) ⊆ dom(σ) and|= σ(C). Similarly, we call a predicate
interpretation ρ a semantic solution forV
C if fpv (C) ⊆ dom(ρ) and ρ |= C.
Remark 1. The language pCSP generalizes over existing languages of constraints.
CHCs can be obtained as a restriction of pCSP where ` ≤ 1 in (1) for all clauses.
We can also define coCHCs as pCSP but with the restriction that m ≤ ` + 1 for
all clauses. A linear CHCs is a pCSP that is both CHCs and coCHCs.
We next extend pCSP to pfwCSP by adding well-foundedness and functionness constraints. A pfwCSP (C, K) consists of– a finite set C of pCSP-clauses over predicate variables and– a kinding function K that maps each predicate variable X ∈ fpv (C) to
its kind: any one of •, ⇓, or λ which respectively represent ordinary, wellfounded, and functional predicate variables.
We write ρ |= WF (X) if the interpretation ρ(X) of the predicate variable X iswell-founded, that is, sort(X) = (es, se) → ? for some se and there is no infinite
sequence ve1 , ve2 , . . . of sequences vei of values of the sorts se such that (evi , vei+1 ) ∈ρ(X) for all i ≥ 1. We write ρ |= FN (X) if X is functional, that is, sort(X) =(es, s) → ? for some se and s, and ρ |= ∀ex : se.(∃y : s.X(ex, y))∧∀y1 , y2 : s.(X(ex, y1 )∧X(ex, y2 ) ⇒ y1 = y2 ) holds. We call a predicate interpretation ρ a semantic
solution for (C, K) if ρ is a semantic solution of C, ρ |= WF (X) for all X suchthat K(X) =⇓, and ρ |= FN (X) for all X such that K(X) = λ. The notion ofsyntactic solution can be similarly generalized to pfwCSP.
Definition 1 (Satisfiability of pfwCSP). The predicate satisfiability problem
of a pfwCSP (C, K) is that of deciding whether it has a semantic solution.
Remark 2. Recall that we assume that the T -formulas ϕ in pCSP clauses do notcontain quantifiers. The assumption, however, is not a restriction for pfwCSP
because we can Skolemize quantifiers using functional predicates.

4

Relational Verification with Constraints

We now present reductions from relational verification problems to pfwCSP, thus
enabling a new route to automation of these problems. We begin with k-safety,
and then move toward liveness and non-determinism, which are thorny problems
in the relational setting. We first provide some basic definitions and notations.

Constraint-based Relational Verification

9

f1 ,. . . ,Vfk , respectively.
Programs. We consider programs P1 ,. . . ,Pk on variables Ve
A state of the program Pi is a valuation of the variables Vi . We represent sucha valuation by a sequence of values ve such that |ev | = |Vei |. We assume that each0
Pi is defined by the predicate Ti (Vei , Vei ) denoting its one-step transition relationi.e., Ti (ev , ve0 ) implies that evaluating Pi one step from the state ve reaches the0state ve . We also assume that there is a predicate Fi (Vei ) that represents the
final states of the program such that Fi (ev ) and Ti (ev , ve0 ) implies ve = ve0 , i.e., theprogram self-loops when it reaches a final state. We say that a state ve (multistep) reaches a final state ve0 in the evaluation of Pi , written ve i ve0 , if there
exists a non-empty finite sequence of states π such that π[1] = ve, π[|π|] = ve0 ,Ti (π[j − 1], π[j]) for all 1 < j ≤ |π|, and Fi (ev 0 ). We write ve i ⊥ if there exists a
non-terminating evaluation from ve in Pi , i.e., if there exists an infinite sequenceof states $ such that $[1] = ve, Ti ($[j − 1], $[j]) for all 1 < j, and ¬Fi ($[j]) for
all 0 < j. We note that a program may be non-deterministic, that is, Ti (ev , ve0 )00
000
and Ti (ev , ve ) may both be true for some ve 6= ve .
4.1

k-Safety

A k-safety property is given by predicates Pre(Ve ) and Post(Ve ) that respectively
denote the pre and the post relations across the k-tuple.
Definition 2 (k-safety). The k-safety property verification problem is to decide
if the following holds:V∀ev = ve1 , . . . , vek .∀ev 0 = ve1 0 , . . . , vek 0 .Pre(ev ) ∧ i∈[k] vei i vei 0 ⇒ Post(ev0 )That is, any k-tuple of final states reachable from a k-tuple of states satisfying
the pre-condition satisfies the post-condition. For instance, the TI-NI verificationfrom Sec. 2.1 is a 2-safety property where P1 and P2 are copies of the same
program, Pre states that the low inputs of the two programs are equal (i.e., x1 =x2 in the example), and Post states that the low outputs of the two programs
are equal (i.e., y1 = y2 in the example).
We now describe a new way to pose the k-safety relational verification problem via constraints written in pfwCSP. We write [k] for the set {1, . . . , k}. We
f1 ,. . . ,V
fk be a k-tuple of vectors,
define P + [k] = {S ⊆ [k] | S 6= ∅}. Let Ve = V
corresponding to the variables of the k programs.
Definition 3 (k-safety through constraints). We define pfwCSP constraints
CS be the set of following clauses:(1) Pre(Ve ) ⇒ inv(Ve )V(2) inv(Ve ) ∧ i∈[k] Fi (Vei ) ⇒ Post(Ve )(3) For each A ∈ P + [k],VV00inv(Ve ) ∧ schA (Ve ) ∧ i∈A Ti (Vei , Vei ) ∧ i∈[k]\A Vei = Vei ⇒ inv(Ve 0 )WW(4) For each A ∈ P + [k], inv(Ve ) ∧ schA (Ve ) ∧ i∈[k] ¬Fi (Vei ) ⇒ i∈A ¬Fi (Vei )WW(5) inv(Ve ) ∧ i∈[k] ¬Fi (Vei ) ⇒ A∈P + [k] schA (Ve ).

10

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

Here, inv and schA (for each A ∈ P + [k]) are ordinary predicate variables.
Roughly, the predicate variables schA describe a scheduler. The scheduler stipulates that when schA (ve1 , . . . , vek ) is true, each Pi such that i ∈ A takes a step fromthe state vei while the others remain still. Note that the scheduler is semantic in
the sense that which programs are scheduled to be executed next can depend on
the current states of the programs. Clauses (1)-(3) assert that inv is an invariant sufficient to prove the given safety property with the scheduler defined byschA ’s. Clauses (4) say that if an inv-satisfying state is such that the processes
in A are allowed to move and some program has not yet terminated, then atleast one process in A has not yet terminated. Clause (5) says that any statesatisfying inv has to satisfy some schA . Clauses (4) and (5) ensure the fairnessof the scheduler, that is, at least one unfinished program is scheduled to makeprogress if there is an unfinished program.
Theorem 1 (Soundness and Completeness of CS ). The given k-tuple ofprograms satisfies the given k-safety property iff CS is satisfiable.
We note that the soundness direction crucially relies on scheduler fairness. The
completeness is with respect to semantic solutions (cf. Def. 1) and it is only “relative” with respect to syntactic solutions: a syntactic solution only exists when
the predicates of the background theory are able to express sufficient invariants
and schedulers (impossible in general for any decidable theory when the classof programs is Turing-powerful as in our case when the background theory of
predicates is QFLIA).
It is important to note that CS is not CHCs because clause (5) has a headdisjunction. CS may be seen as a constraint-based formulation of the approach
proposed in [51]. However, their approach requires the user to provide sufficient
predicates manually and is not fully automated, while our approach can fully
automatically solve the problems by constraint solving (cf. Sec. 5).
Example 1. The formalization allows flexible scheduling. For instance, for the TINI example from Sec. 2.1, our approach is able to infer the predicate substitutionthat maps sch{1} , sch{2} , and sch{1,2} to λVe .h1 ∧¬h2 ∧z1 = 2z2 , λVe .¬h1 ∧h2 ∧z2 =
2z1 , and λVe .(h1 ∧ ¬h2 ⇒ z1 + 1 = 2z2 ) ∧ (¬h1 ∧ h2 ∧ z2 + 1 = 2z1 ) respectively,
where Ve is the list of the variables in the two program copies. The inferredpredicates stipulate that the copy with h = true is scheduled to execute theloop two times per every loop iteration of the copy with h = false. Appendix A
shows the pfwCSP encoding of the example. A solution generated by PCSat is
also shown in Appendix B.
4.2

Co-termination

Intuitively, co-termination means that if one program terminates, then a second
program must terminate [6,10]. This can also be thought of as a form of relationaltermination problem.6
6The property has also been called relative termination [31].

Constraint-based Relational Verification

11

Definition 4 (Co-Termination). The co-termination verification problem isto decide if for all ve1 , ve2 such that Pre(ve1 , ve2 ), if ve1 1 ve10 then ve2 6 2 ⊥.
Roughly, the property says that from any pair of states related by Pre, if P1
terminates, then P2 must also terminate. Note that this is an asymmetric property. A symmetric version can be obtained by also asserting the property withthe positions of the two programs exchanged. The symmetric version implies,
assuming that there is at least one execution from any Pre-related state, thatfrom any pair of Pre-related states, all executions from one state terminate iff
all executions from the other one do as well. We now present an encoding ofconditional co-termination in pfwCSP.
f1 , Vf2 . We
Definition 5 (Co-termination through constraints). Let Ve = V
define pfwCSP constraints CCoT be the set of following clauses:(1) Pre(Ve ) ∧ fnb(Ve , b) ⇒ inv(0, b, Ve )f1 ) ∧ ¬F2 (Vf2 ) ⇒ (−b ≤ d ∧ d ≤ b ∧ b ≥ 0)(2) inv(d, b, Ve ) ∧ ¬F1 (V0f2 , Vf2 ) ∧ (F1 (Vf1 ) ∨ F2 (Vf2 ) ∨ d0 = d − 1) ⇒(3a) inv(d, b, Ve ) ∧ schFT (d, b, Ve ) ∧ T2 (V00f1 , Vf2 )inv(d , b, V
0ef1 , Vf1 ) ∧ (F1 (Vf1 ) ∨ F2 (Vf2 ) ∨ d0 = d + 1) ⇒(3b) inv(d, b, V ) ∧ schTF (d, b, Ve ) ∧ T1 (V00f1 , Vf2 )inv(d , b, V
0
0
0
0
e
f1 , Vf1 ) ∧ T2 (Vf2 , Vf2 ) ⇒ inv(d, b, V
f1 , Vf2 )(3c) inv(d, b, V ) ∧ schTT (d, b, Ve ) ∧ T1 (Vf1 ) ⇒ ¬F2 (Vf2 )(4a) inv(d, b, Ve ) ∧ schFT (d, b, Ve ) ∧ ¬F1 (V
e
e
f
f1 )
(4b) inv(d, b, V ) ∧ schTF (d, b, V ) ∧ ¬F2 (V2 ) ⇒ ¬F1 (VW
f1 ) ∨ ¬F2 (Vf2 )) ⇒
(5) inv(d, b, Ve ) ∧ (¬F1 (Vscha (d, b, Ve )a∈{TT,FT,TF}
00f1 ) ∧ ¬F2 (Vf2 ) ∧ T2 (Vf2 , Vf2 ) ⇒ wfr(Vf2 , Vf2 )(6) inv(d, b, Ve ) ∧ F1 (VHere, schTT , schFT , and schTF are 2-specialization of the k-safety scheduler ofDef. 3. Clauses (3x)’s are similar to (3) of Def. 3 and assert that inv is aninvariant under the scheduler. Clauses (4x)’s and (5), like (4) and (5) of Def. 3,
are used to ensure the scheduler fairness. However, they are insufficient for cotermination as a non-terminating copy can be scheduled indefinitely leaving theother copy unscheduled. Clauses (1) and (2) are added to amend the issue. In(1), fnb is a functional predicate variable that is used to select a bound b, and(2) asserts that the difference d between the numbers of steps taken by the twocopies is within b in any state in inv when neither copy has terminated. Notethat d is initialized to 0 by (1) and properly updated in (3x)’s. Finally, by using
the well-founded predicate variable wfr, (6) asserts that if P1 has terminated,then so must eventually P2 .
Theorem 2 (Soundness and Completeness of CCoT ). The given pair ofprograms co-terminate iff CCoT is satisfiable.
As with Theorem 1, the soundness direction relies on scheduler fairness.
Example 2. Via the encoding, our PCSat tool is able to verify the symmetricco-termination example from Sec. 2.1 by automatically inferring the solution
described there. For space, the concrete constraint set and solution are given in
Appendix C and D.

12

4.3

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

Generalized Non-Interference

We now turn to another relational property that cannot simply be captured byk-safety or co-termination. So-called termination-insensitive (resp. -sensitive)
generalized non-interference (resp. TI-GNI, TS-GNI) are ∀∃ hyperproperties:
from any pre-related pair of states whenever one side can take a move to a poststate, there must be a way for the other side to also move to a post state such thatthe post-relation holds. As remarked in Sec. 2, verifying GNI requires reasoning
about both demonic (i.e., for all) and angelic (i.e., exists) non-determinism.
Definition 6 (TI/TS-GNI). The GNI verification problem is to decide if thefollowing holds. If Pre(ve1 , ve2 ) and ve1 1 ve1 0 then (TI-GNI) (∃ve2 0 .ve2 2 ve2 0 ∧Post(ve1 0 , ve2 0 )) ∨ ve2 2 ⊥; or (TS-GNI) ∃ve2 0 .ve2 2 ve2 0 ∧ Post(ve1 0 , ve2 0 ).
Note that our definition is parameterized by Pre and Post. The standard GNI
definitions [41] can be obtained by letting P1 and P2 be copies of the same target
program and letting Pre be the predicate equating the low inputs of the copies
and Post be the predicate equating the low outputs of the copies.
To formalize the pfwCSP encodings of the GNI verification problems, we define a relation U2 to be one such that T2 (ev , ve0 ) ⇔ ∃r.U2 (r, ve, ve0 ) and U2 (r, ve, ve0 ) ∧00
000
U2 (r, ve, ve ) ⇒ ve = ve . Roughly, U2 is a function version of the transition relation
T2 with the extra parameter r to make the non-deterministic choices explicit.
We now show the pfwCSP encodings of TI-GNI and TS-GNI. The key idea
is to augment the encodings for k-safety and/or co-termination with functional
predicate variables and prophecy variables that respectively represent the nondeterministic choices of the angelic side (i.e., P2 ) and the final outputs of thedemonic side (i.e., P1 ).
Definition 7 (TI-GNI through constraints). We define pfwCSP constraints
CTIGNI as CS in Def. 3 for k = 2 but with the following modifications:(m1) The parameters representing the inputs and outputs of P1 are extended with
f1 |. Accordingly, each occurrence of V
f1 isprophecy variables pe where |ep | = |V00f1 , and each occurrence of V
f1 is replaced by pe0 , V
f1 .
replaced by pe, V
f1 , Vf2 ) ⇔ Pre(Vf1 , Vf2 ),(m2) Pre is replaced by Pre 0 which is defined by Pre 0 (ep, Vi.e., the prophecy values are unconstrained in the pre-condition.
f1 ) ⇔ F1 (Vf1 ).
(m3) F1 is replaced by F10 defined by F10 (e
p, V
0
0
0
0
0 f
f
f1 , Vf1 ) ∧ pe = pe0 .
(m4) T1 is replaced by T1 defined by T1 (ep, V1 , pe , V1 ) ⇔ T1 (Vf1 , Vf2 ) ⇔ (ef1 ⇒ Post(Vf1 , Vf2 )),(m5) Post is replaced by Post 0 defined by Post 0 (ep, Vp=Vi.e., if the prophecy was correct then the original post-condition must hold.
00
f2 , Vf2 ) is replaced by fnr(ef2 , r)∧U2 (r, V
f2 , Vf2 ) where(m6) Each occurrence of T2 (Vp, V
fnr is a functional predicate variable.
Modifications (m1)-(m5) concern prophecy variables. They are initialized arbitrarily as shown in (m2), propagated unmodified through the transitions asshown in (m4), and finally checked if they match P1 ’s outputs in (m5). Modification (m6) adds functional predicate variables to express the angelic nondeterministic choices of P2 . The functional predicate variables shift the onus ofConstraint-based Relational Verification

13

making the right choices to the solver’s task of discovering sufficient assignments
to them. Importantly, the functional predicate takes the prophecy variables asparameters, thus allowing dependence on the final outputs of the demonic side.
Definition 8 (TS-GNI through constraints). We define pfwCSP constraints
CTSGNI as CCoT in Def. 5 but with modifications of Def. 7 except (m3) and (m5),and with the following modifications:f1 ) ⇔ F1 (Vf1 ) ∧ pe = V
f1 .
(m3’) F1 is replaced by F10 defined by F10 (e
p, V
0
f
f
f
f
f
f
(m5’) The clause inv(ep, V1 , V2 ) ∧ F1 (ep, V1 ) ∧ F2 (V2 ) ⇒ Post(V1 , V2 ) is added.
CTSGNI is similar to CTIGNI except that it contains the difference bound and wellfoundedness constraints to handle the “co-termination” aspect of TS-GNI, i.e., if
P1 terminates and makes an output then P2 must also be able to terminate andmake a matching output. One subtle aspect of the encoding is that (m3’) modifies
the final state predicate for P1 to enforce co-termination only when the prophecy
is correct. However, it is worth noting that TS-GNI is not a conjunction of TIGNI and co-termination. For instance, the GNI example from Sec. 2.1 satisfies
TS-GNI but does not satisfy co-termination.
Theorem 3 (Soundess and Completeness of of TI-GNI). The given pairof programs satisfy TI-GNI iff CTIGNI is satisfiable.
Theorem 4 (Soundess and Completeness of TS-GNI). The given pair ofprograms satisfy TS-GNI iff CTSGNI is satisfiable.
The soundness directions are proven by “determinizing” the angelic choices bysolutions to the functional predicate variables and reducing the argument tothose of k-safety and co-termination. The completeness directions are proven by“synthesizing” sufficient angelic choice functions from program executions.
Example 3. Via the encoding, our PCSat tool is able to verify the TS-GNI example from Sec. 2.1 by automatically inferring not only the functional predicate
described there but also relational invariants and well-founded relations given in
the appendix. For space, the concrete constraint set is also given in the appendix.
Remark 3. The angelic non-determinism encoding can be optimized by using
head disjunctions when the non-determinism is finitary (i.e., maxve|{ev 0 | T2 (ev , ve0 )}|is finite) instead of using functional predicate variables. For this, we modify
clauses (3) and (3x)’s of Def. 7 and 8 to contain multiple positive occurrences of
inv where each occurrence represents one of the finitely many possible choices.
Remark 4. Recall that we allow any program to be non-deterministic. The ksafety and co-termination encodings treat non-determinism in all programs as
demonic, whereas the GNI encodings treat those in one program (i.e., P1 ) as
demonic and those in the other program (i.e., P2 ) as angelic. In general, an
arbitrary program can be made angelic by applying the transformation done in
the angelic side of GNI encodings (to factor out non-determinism).

14

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

5Constraint Solving Method for pfwCSP

We describe a CEGIS-based method for finding a (syntactic) solution of the given
pfwCSP (C, K). Our method iterates the following phases until convergence.
The iteration maintains and builds a sequence σ of candidate solutions and asequence E of example instances where E (i) are ground clauses obtained from C by
instantiating the term variables and serve as a counterexample to the candidate
solution σ (i−1) , for each i-th iteration. The iteration starts from E (1) = ∅.
Synthesis Phase: We check if (E (i) , K) is unsatisfiable. If so, we stop by
returning E (i) as a genuine counterexample to the input problem (C, K). Otherwise, we use the synthesizer ST B (cf. Sec. 5.1) to find a solution σ (i) of (E (i) , K),
which will be used as the next candidate solution.
Validation Phase: We check if σ (i) is a genuine solution to (C, K) by using
an SMT solver. If so, we stop by returning σ (i) as a solution. Otherwise, for eachclause c ∈ C not satisfied by σ (i) , we obtain a term substitution θc such that
dom(θc ) = ftv (c) and 6|= θc (σ (i) (c)). We then update the example set by adding
a new example instance for each unsatisfied clause (i.e., E (i+1) = E (i) ∪ { θc (c) |c ∈ C∧ 6|= σ (i) (c) }), and proceed to the next iteration.
The above procedure satisfies the usual progress property of CEGIS: discovered counterexamples and candidate solutions are not discovered again in succeeding iterations. Furthermore, as discussed in Sec. 5.1, by carefully designing
the synthesizer ST B by incorporating stratified CEGIS, we achieve completeness in the sense of [34, 56]: if the given pfwCSP (C, K) has a syntactic solution
expressible in the stratified families of templates, a solution of the pfwCSP is
eventually found by the procedure. In Sec. 5.1, we discuss the details of the synthesis phase. There, for space, we focus on the theory of quantifier-free linear
integer arithmetic (QFLIA). For space, we defer the details of the unsatisfiability
checking process to Appendix K.
Remark 5. The implementation described in Sec. 6 contains an additional phasecalled resolution phase for accelerating the convergence. There, we first apply
unit propagation repeatedly to the given E (i) to obtain positive examples E (i)+of the form X(ev ) and negative examples E (i)− of the form ¬X(ev ). We thenrepeatedly apply resolution principle to the clauses in the input clauses C andthe clauses E (i)+ ∪ E (i)− to obtain additional positive and negative examples.
5.1

Predicate Synthesis with Stratified Families of Templates

We describe our candidate solution synthesizer ST B . ST B performs a templatebased search for a solution to the given example instances. As we shall show, ourapproach allows searching for assignments to all predicate variables (of all threekinds) in the given instance which is important because satisfying assignments todifferent predicate variables often inter-dependent. There, however, is a trade-off
between expressiveness and generalizability. With less expressive templates likeintervals, we may miss actual solutions. But with very expressive templates likepolyhedra, there could be many solutions, and a solution thus returned is liable

Constraint-based Relational Verification

15

Stratified Template Family for Ordinary Predicate Variables:
Par(X)Vnc
W•
TX(nd , nc, ac, ad ) , λ(x1 , . . . , xar(X) ). nd
k=1 ci,j,k · xk ≥ 0
j=1 ci,j,0 +i=1
Vnc Par(X)
V
(
|c
|
≤
ac)
∧
|c
φ•X (nd , nc, ac, ad ) , ndi,j,0 | ≤ ad
i,j,k
k=1
j=1
i=1
Stratified Template Family for Well-Founded Predicate Variables:W
Vnp Vnl⇓x))∧x) ≥ 0 ∧ ( np
TX(np, nl , nc, rc, rd , dc, Wdd ) , λ(ex, ye). W
i=1 Di (ek=1 ri,k (e
i=1
V
np
np
(D
(e
y
)
⇒
DEC
x, ye)))
D
(e
x
)
∧
D
(e
y
))
∧
(
( np
j
i,j (eijj=1
j=1
Par(X)/2
Vnp Vnl i=1
(
|c
|
≤
rc)
∧
|c
|
≤
rd
∧
φ⇓
(np,
nl
,
nc,
rc,
rd
,
dc,
dd
)
,
i,k,`
i,k,0
X
i=1 Vk=1 P`=1
Vnp
ar(X)/2 0
nc
0
(
|c
|
≤
dc)
∧
|c
|
≤
dd
i,k,`
i,k,0
`=1
Vk−1
Wi=1 k=1ri,` (ex) ≥ rj,` (ey ))(ri,k (ex) > rj,k (ey ) ∧ `=1
DEC i,j (ex, ye) , nl
k=1
Par(X)/2 0
Par(X)/2V0c+cri,k (ex) , ci,k,0 + `=1
ci,k,` · x`
Di (ex) , nci,k,` · x` ≥ 0`=1
k=1 i,k,0Stratified Template Family for Functional Predicate Variables:
λTX(nd , nc, dc, dd , ec, ed ) , λ(ex, r).r = if D1 (ex) then e1 (ex) else if D2 (ex) then e2 (ex) · · ·else if Dnd−1 (ex) then end−1 (ex) else end (ex)
VPar(X)−1|ci,j | ≤ ec) ∧ |ci,0 | ≤ ed ∧φλX (nd , nc, ec, ed , dc, dd ) , nd
i=1 (
Vnd−1
Vj=1
Par(X)−1 0nc|c| ≤ dc) ∧ |c0i,j,0 | ≤ dd
k=1
i=1
j=1 (
Par(X)−1
Vnc i,j,k
Par(X)−1 00ei (ex) , ci,0 + j=1
ci,j · xj
Di (ex) , j=1 ci,j,0 + k=1
ci,j,k · xk ≥ 0
Fig. 2. Stratified Families of Templates

to overfitting, i.e., the solution to the example instances becomes too specific
to be an actual solution to the original input clauses. [45] discusses a similar
overfitting issue in the context of grammar-based synthesis.
Our remedy to the issue is stratified families of predicate templates, inspiredby a similar approach proposed in the context of predicate abstraction with
CEGAR [34, 56]. Initially, we assign each predicate variable a less expressive
template and gradually refine it in a counterexample-guided manner: if no solution exists in the current template, we generate and analyze an unsat core
to identify the parameters of the families of templates that should be updated.
The stratification of templates thus automatically pushes the template to an expressive one (e.g., polyhedra) when it needs to. Importantly, with our approach,expressive templates are not always used but only when they should be used.
Stratified Families of Templates We have designed three stratified familiesof templates shown in Fig. 2, respectively for ordinary (•), well-founded (⇓), andfunctional (λ) predicate variables. First, for each ordinary predicate variable X,•
we prepare the stratified family of templates TX(nd , nc, ac, ad ) with unknowns
ci,j,k ’s to be inferred and its accompanying constraint φ•X (nd , nc, ac, ad ). The•
body of TX
is a DNF with affine inequalities as atoms. The parameter nd (resp.
nc) is the number of disjuncts (resp. conjuncts). The parameter ac is the upperbound of the sum of the absolute values of coefficients ci,j,k (k > 0), and ad isthe upper bound of the absolute value of ci,j,0 .
Secondly, for each functional predicate variable X, we prepare the strati⇓
fied family of templates TX(np, nl , nc, rc, rd , dc, dd ) with unknowns ci,j,k ’s and16

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen⇓
c0i,j,k ’s and its accompanying constraint φ⇓X (np, nl , nc, rc, rd , dc, dd ). TX
represents the well-founded relation induced by a piecewise-defined lexicographic affine
ranking function [2, 40, 40, 60, 61] where ri,j is the affine ranking function template for the j-th lexicographic component of the i-th region specified by thediscriminator Di . The parameter np (resp. nl ) is the number of regions (resp.
lexicographic components). The parameters rc, rd , dc, dd are the upper bounds•of (the sums of) the absolute values of unknowns, similar to ac and ad of TX.
⇓
The first conjunct of TX asserts that the return value of each ranking functions
is non-negative. The second and the third conjuncts assert that the discriminators cover all relevant states. Note that discriminators may overlap, and forsuch overlapping regions, the maximum return value of the ranking functions isused. The fourth conjunct asserts that the return value of the piecewise-definedranking function strictly decreases from x
e to ye. Here, DEC i,j (ex, ye) asserts thatthe return value of the lexicographic ranking function for the i-th region at xe
is greater than that for the j-th region at ye. It follows that for any substitu⇓⇓) represents a well-founded relation. Our, θ(TX
tion θ for the unknowns in TX⇓
implementation PCSat uses a refined version of TX
shown in Appendix L.
Finally, for each functional predicate variable X, we prepare the stratified
λfamily of templates TX(nd , nc, dc, dd , ec, ed ) with unknowns ci,j ’s and c0i,j,k ’s
λand its accompanying constraint φλF (nd , nc, dc, dd , ec, ed ). TX
characterizes apiecewise-defined affine function with discriminators D1 , . . . , Dnd−1 and branch
expressions e1 , . . . , end . The parameter nc is the number of conjuncts in eachdiscriminator. The parameters dc, dd , ec, ed are the upper bounds of (the sums•
. Note that forof) the absolute values of unknown, similar to ac and ad of TXλλany substitution θ for the unknowns in TX , θ(TX )(ex, r) expresses a total functionthat maps x
e to r.
Next, we give the details of the candidate solution synthesis process. Let
pe ∈ Zn where n is the number of parameters summed across all templates, and
αp) (for α ∈ {•, ⇓, λ}) project the corresponding parameters.
(ep) and φα
let TXX (eEach pe ∈ Zn induces a solution space Je
pK , {T (ep)[θ] | θ |= Con(ep)} where
V
K(X)
K(X)
T (e
p)[θ] , {X 7→ θ(TX (ep)) | X ∈ fpv (C)} and Con(ep) , X∈fpv (C) φX (ep).
Let pe1 ≤ pe2 be the point-wise ordering. Note that Je
pK is a finite set forany pe ∈ Zn , and pe1 ≤ pe2 implies Je
p1 K ⊆ Je
p2 K. We start the CEGIS processwith some small initial parameters pe(0) (the parameters will be maintained asa state of the CEGIS process). The synthesis phase of each iteration tries tofind a solution θ ∈ Je
p(i) K to the given example instances (E, K) where pe(i) are
the current parameters.
This is done by using an SMT solver for QFLIA toVfind θ satisfying T (ep(i) )[θ](E) ∧ θ(Con(ep(i) )). If such θ is found, we return(i)
T (ep )[θ] as the candidate solution for the next validation phase of the CEGIS
process. Note that, by construction of the templates, the solution is guaranteed
to assign each well-founded (resp. functional) predicate variable a well-founded
relation (resp. total function). Otherwise, no solutions to the given example
instances (E, K) can be found in Je
p(i) K, and we update the parameters to some
(i+1)
(i)
(i+1)
pe
> pe such that Jep
K contains a solution for (E, K). Here, it is important
to do the update in a fair manner [34,56], that is, in any infinite series of updates

Constraint-based Relational Verification17pe(0) , pe(1) , . . . , every parameter is updated infinitely often (the details are deferred
to below). By the progress property and the fact that every Je
pK is finite, thisensures that every parameter is updated infinitely often in an infinite series of
CEGIS iterations. We thus obtain the following property.
Theorem 5. Our CEGIS-procedure based on stratified families of templates iscomplete in the sense of [34, 56]: if there is pe and σ ∈ Je
pK such that σ is a
syntactic solution to the given pfwCSP (C, K), a syntactic solution to (C, K) is
eventually found by the procedure.
Note that, while the solution space of each stratum (i.e., Je
p(i) K) is finite, ourprocedure searches the infinite solution space obtained by taking
S the(i)infinite
union of the solution spaces of the template family strata (i.e., i∈ω Je
p K).
Remark 6. Our template-based synthesis simultaneously finds ordinary, wellfounded, and functional predicates that are mutually dependent through thegiven (E, K). This means that templates for different kinds of predicate variables
are updated in a synchronized and balanced manner, which benefits the synthesis of mutually dependent witnesses for a relational property (see Appendix B,
D, and F for examples).
Updating Parameters of Template Families via Unsat Cores. We now describe
the parameter
update process. We first obtain the unsat core of the unsatisfiV
ability of T (ep(i) )[θ](E) ∧ θ(Con(ep(i) )) from the SMT solver. We then analyze
the core to obtain the parameters of template families, such as the number ofconjuncts and disjuncts, that have caused the unsatisfiability. Here, there could
be a dependency between predicate variables and in such a case our unsat core
analysis enumerates all the involved predicate variables from which we obtain
the parameters of template families to be updated. We then increment theseparameters in some fair manner, by limiting the maximum differences between
different parameters to some bounded threshold, and repeatedly solve the resulting constraint until a solution is found. Thus, the parameters of stratified
families of templates are grown on-the-fly guided by the reasons for unsatisfiability. We found that a careful design of parameter update strategies importantfor scaling the stratified CEGIS to hard relational verification problems. The
manual tuning, however, is tiresome and suboptimal. We leave as future work
to investigate methods for automatic tuning of parameter update strategies.

6

Evaluation

To evaluate the presented verification framework, we have implemented PCSat,a satisfiability checking tool for pfwCSP based on stratified CEGIS. PCSat supports the theory of Booleans and the quantifier-free theory of linear inequalities
over integers and rationals. The tool is implemented in OCaml, using Z3 [42] as
the backend SMT solver. We ran the tool on a diverse collection of 20 relationalverification problems, consisting of k-safety, co-termination, and GNI problems.

18

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

Though we have manually reduced them to pfwCSP using the presented method
in Sec. 4, this process can be easily automated. The full benchmark set is provided in Appendix M. All experiments have been conducted on 3.1GHz Intel
Xeon Platinum 8000 CPU and 32 GiB RAM with the time limit of 600 seconds.
The experimental results are summarized in Table 1. The columns “Time (s)”and “#Iters” respectively show elapsed wall clock time in seconds and numbersof CEGIS iterations. PCSat solved 15 verification problems fully automaticallyand 5 problems labeled with the symbol † and/or ‡ semi-automatically. For
the 4 problems labeled with †, we manually provided small hints for invariant
synthesis (interested readers are referred to Appendix M). The provided hints
for all but SquareSum are non-relational invariants that can be inferred prior
to relational verification by using a CHCs solver or an invariant synthesizer.
For the 2 problems labeled with ‡, we manually chose the initial value for theparameters of the template family for ordinary predicate variables to reduce theelapsed time. This can be automated by running PCSat with different initialvalues in parallel.
The problems DoubleSquareNI_h**, HalfSquareNI, ArrayInsert, and SquareSum
are k-safety verification problems obtained from [51] that require non-lock-stepscheduling.7 The problems DoubleSquareNI_h** are generated from Example 1
by a case analysis of the valuation for the boolean variables h1 and h2 . PCSat solved all the k-safety problems but SquareSum fully automatically. The tool
Pdsc proposed in [51] can verify them but requires the user to provide theatomic predicates for expressing relational invariants and schedulers. The problems CotermIntro1 and CotermIntro2 are asymmetric co-termination problems
obtained from the symmetric problem in Example 2 and are verified by PCSat
fully automatically. The problems TS_GNI_h** are generated from Example 3
by a case analysis and are verified by PCSat with small non-relational hints.
We have also tested PCSat on various TS-GNI (SimpleTS_GNI1, SimpleTS_GNI2,
InfBranchTS_GNI) and TI-GNI problems (TI_GNI_h**) and obtained promising
results. As far as we know, no existing tools can verify these non-k-safety relational problems.
Furthermore, manual inspection of the PCSat’s output logs for the GNI
problems that required hints revealed that the functional predicate synthesis
appears to be the main bottleneck of the current version. In fact, we confirmedthat the problems can be solved in less than 10 seconds if appropriate functional
predicates for angelic non-determinism are manually provided. As future work,
we plan to investigate methods for improved functional predicate synthesis.

7

Related Work

7.1

Relational Verification

There has been substantial work on verifying relational properties. They include
program logics, type systems, or program analysis frameworks such as abstract
7

We omitted ArrayIntMod from [51] because its verification requires the theory ofarrays which the current version of PCSat does not fully support.

Constraint-based Relational Verification

19

Table 1. Experimental results of PCSat on the relational verification benchmarks
Program
Time (s) #Iters ProgramTime (s) #Iters
DoubleSquareNI_hFT 17.762
42 HalfSquareNI
11.85335
DoubleSquareNI_hTF 26.495
55 ArrayInsert‡
118.671
73
DoubleSquareNI_hFF
2.944
9 SquareSum†‡
337.596
117
DoubleSquareNI_hTT
4.055
11 SimpleTS_GNI1
5.397
14
CotermIntro1
19.32280 SimpleTS_GNI2
8.919
26
CotermIntro2
15.871
73 InfBranchTS_GNI
2.607
4
TS_GNI_hFT†
47.083
78 TI_GNI_hFT†
4.389
16
TS_GNI_hTF
5.076
17 TI_GNI_hTF
2.277
6
TS_GNI_hFF
7.174
24 TI_GNI_hFF
2.9686
TS_GNI_hTT†
23.495
53 TI_GNI_hTT
4.148
22

interpretation and model checking [1, 5, 9, 19, 25, 53, 62], program transformation
approaches such as self-composition or product programs [4,7,15,20,21,43,48,55,
58,64], and various other approaches [3,18,23,47,59]. We refer to [44] for an excellent survey. However, most prior automatic approaches address only the k-safety
fragment [17,55] and cannot verify non-k-safety (actually, not even hypersafety)
properties such as co-termination, TS-NI, TI-GNI, and TS-GNI [6, 11, 41]. The
only exception that we are aware is the recent work by Coenen et al. [19] that
proposes a sound method for automatically verifying ∀∃ hyperproperties suchas GNI for finite state systems. To our knowledge, we are the first to propose asound-and-complete approach to automatically verifying these non-hypersafety
properties for infinite state programs.8
A key task in many relational verification methods, including ours, is thediscovery of relational invariants which relate the states of multiple program
executions. While most prior approaches are limited to fixed execution schedule(or alignment) such as lock-step and sequential [7, 8, 20, 21, 43, 55, 58], a recent
work by Shemer et al. [51] has proposed a k-safety property verification methodthat automatically infers fair schedulers sufficient to prove the goal property.
Importantly, the schedulers in their approach can be semantic in which the
choice of which program to execute can depend on the states of the programs
as opposed to the classic syntactic schedulers such as lock-step and sequentialthat can only depend on the control locations. Our approach also infers such fairsemantic schedulers, and as remarked before, they enable solving instances likedoubleSquare that are difficult for previous approaches. However, [51] requires
the user to provide appropriate atomic predicates and is not fully automatic.
By contrast, our approach soundly and completely encodes the problem as a
8

However, [19] can verify (relational) temporal properties, whereas we only support
functional properties that are given by pre- and post-conditions of whole program
runs. We leave as future work to investigate methods for verifying relational temporal
properties of infinite state programs.

20

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

constraint satisfaction problem and fully automatically verifies hard instances
like doubleSquare by constraint solving.
Furthermore, our work extends the fair semantic scheduler synthesis to beyond k-safety problems like co-termination, TI-GNI and TS-GNI, in a soundand complete manner. We note that the extensions are non-trivial and involves
delicate uses of functional predicate variables and well-founded predicate variables to ensure scheduler fairness in the presence of non-termination as well as
uses of prophecy variables and functional predicate variables to handle angelic
non-determinism. The higher-degree of automation and the extension to nonk-safety properties are thanks to the expressive power of our novel constraint
framework pfwCSP.
7.2

Predicate Constraint Solving

Our pfwCSP solving technique builds on and generalizes a number of techniquesdeveloped for CHCs solving as well as invariant and ranking function discovery.
Most closely related to our constraint solving method are CEGIS-based [52] anddata-driven approaches to solving CHCs [14,22,24,26,27,39,45,46,49,50,65]. As
remarked before, the new pfwCSP framework is strictly more expressive than
CHCs and extending the prior techniques to the new framework is non-trivial.
Our stratified CEGIS is inspired by the idea of stratified languages of predicates proposed in the context of predicate abstraction with CEGAR [34, 56]. It
is also similar in spirit to the work by Padhi et al. [45], but they use a stratified
family of grammars. Also none of these prior works use unsat cores for updating
the language/grammar stratum, synthesize well-founded relations and functional
predicates, or support non-Horn clauses.
Our class of pfwCSP constraints is related to existentially-quantified Hornclauses (E-CHCs) introduced by Beyene et al. [12]. E-CHCs does not havenon-Horn clauses or functional predicate variables. However, it has disjunctive well-foundedness constraints which are similar to our well-founded predicate
variables. Also, existential quantifiers can be used to encode head disjunctions
and functional predicates. We conjecture that pfwCSP and E-CHCs are interreducible, but it is not trivial to fill the gap. Also, inter-reducibility is a desirable
feature: different formats may have different benefits. For relational verification,
as we have shown, pfwCSP enables direct sound-and-complete encodings of the
problems. For instance, head disjunctions allow direct encoding of scheduler
fairness and finitary angelic non-determinism (cf. Remark 3). And, functional
predicate variables can be explicitly given necessary-and-sufficient parameters
to encode angelic non-determinism and difference bounds for ensuring scheduler
fairness in the presence of non-termination. The tight encodings also lead to
reduction in search space and benefited the constraint solving.

8

Conclusion

We have introduced the class pfwCSP of predicate constraint satisfaction problems that generalizes CHCs with arbitrary clauses, well-foundedness constraints,

Constraint-based Relational Verification21

and functionality constraints. We have then established a program verification
framework based on pfwCSP by showing that (1) pfwCSP can soundly-andcompletely encode various classes of relational problems of infinite-state nondeterministic programs, including hard instances of k-safety, co-termination,and termination-sensitive generalized non-interference that benefit from statedependent scheduling/alignment (Theorems 1–4), and (2) existing CHCs solving
and invariants/ranking function synthesis techniques can be adopted to pfwCSP
solving and further improved with the idea of stratified CEGIS for simultaneously achieving completeness (Theorem 5) and efficiency.
In future work we plan to investigate ways to improve functional predicate
synthesis, automatic tuning of parameter update strategies for constraint solving,
and whether a constraint-based approach (and the techniques presented in thepresent paper) can be extended to reason about relational temporal properties
such as the ones expressed in hyper temporal logics [16, 25].
Acknowledgments. We thank the anonymous reviewers for their suggestions.
This work was supported by ONR grant # N00014-17-1-2787, JST ERATO
HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and
JSPS KAKENHI Grant Numbers 17H01720, 18K19787, 19H04084, 20H04162,
20H05703, and 20K20625.

References
1. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic forhigher-order programs. J. Funct. Program. 29 (2019)
2. Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: SAS ’10. pp.
117–133. Springer (2010)
3. Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels.
In: PLDI (2017)
4. Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional
programs by first-order refinement. In: PEPM (2015)
5. Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: POPL (2017)
6. Barthe, G.: An introduction to relational program verification (2020)
7. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs.
In: FM (2011)
8. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition.
In: CSFW (2004)
9. Benton, N.: Simple relational correctness proofs for static analyses and programtransformations. In: POPL (2004)
10. Beringer, L.: Relational bytecode correlations. J. Log. Alg. Meth. Pro. 79(7) (2010)
11. Beringer, L., Hofmann, M.: Secure information flow and program logics. Arch.
Formal Proofs (2008)
12. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Hornclauses. In: CAV (2013)

22

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

13. Bjørner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers
for program verification. In: Fields of Logic and Computation II: Essays Dedicatedto Yuri Gurevich on the Occasion of His 75th Birthday (2015)
14. Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement typediscovery for higher-order functional programs. In: TACAS (2018)
15. Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment
for equivalence checking. In: PLDI (2019)
16. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez,
C.: Temporal logics for hyperproperties. In: POST (2014)
17. Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF (2008)
18. Clochard, M., Marché, C., Paskevich, A.: Deductive verification with ghost monitors. PACMPL 4(POPL) (2020)
19. Coenen, N., Finkbeiner, B., Sánchez, C., Tentrup, L.: Verifying hyperliveness. In:
CAV (2019)20. Ádám Darvas, Hähnle, R., Sands, D.: A theorem proving approach to analysis of
secure information flow. In: SPC (2005)
21. Eilers, M., Müller, P., Hitz, S.: Modular product programs. TOPLAS 42(1) (2020)
22. Ezudheen, P., Neider, D., D’Souza, D., Garg, P., Madhusudan, P.: Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2(OOPSLA) (2018)
23. Farzan, A., Vandikas, A.: Automated hypersafety verification. In: CAV (2019)24. Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In:
CAV (2018)
25. Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL
and HyperCTL∗ . In: CAV (2015)
26. Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: A robust framework forlearning invariants. In: CAV (2014)
27. Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision
trees and implication counterexamples. In: POPL (2016)
28. Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using
extremal counterexamples. In: PLDI (2015)
29. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)
30. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification
framework. In: CAV (2015)31. Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: CADE (2013)
32. Hojjat, H., Rümmer, P.: The Eldarica horn solver. In: FMCAD (2018)33. Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: verifying functional programs
using abstract interpreters. In: CAV (2011)34. Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS (2006)
35. Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J.
Comput. 4 (1975)
36. Kahsai, T., Rümmer, P., Sanchez, H., Schäf, M.: JayHorn: A framework for verifying Java programs. In: CAV (2016)
37. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higherorder model checking. In: PLDI (2011)
38. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive
programs. In: CAV (2014)
39. Krishna, S., Puhrsch, C., Wies, T.: Learning invariants using decision trees. CoRR
abs/1501.04725 (2015)

Constraint-based Relational Verification

23

40. Leike, J., Heizmann, M.: Ranking templates for linear loops. LMCS 11(1) (2015)41. McCullough, D.: Noninterference and the composability of security properties. In:
SP (1988)
42. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS (2008)
43. Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: ESORICS (2006)
44. Naumann, D.A.: Thirty-seven years of relational hoare logic: remarks on its principles and history. CoRR abs/2007.06421 (2020)
45. Padhi, S., Millstein, T.D., Nori, A.V., Sharma, R.: Overfitting in synthesis: Theory
and practice. In: CAV (2019)46. Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference withlearned features. In: PLDI (2016)
47. Pick, L., Fedyukovich, G., Gupta, A.: Exploiting synchrony and symmetry in relational verification. In: CAV (2018)
48. Reynolds, J.C.: The craft of programming. Prentice Hall (1981)
49. Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data
driven approach for algebraic loop invariants. In: ESOP (2013)
50. Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: SAS (2013)
51. Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: CAV (2019)52. Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorialsketching for finite programs. In: ASPLOS (2006)
53. Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In:
PLDI (2016)
54. Terauchi, T.: Dependent types from counterexamples. In: POPL (2010)
55. Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: SAS(2005)
56. Terauchi, T., Unno, H.: Relaxed stratification: A new approach to practical complete predicate refinement. In: ESOP (2015)
57. Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP(2009)
58. Unno, H., Kobayashi, N., Yonezawa, A.: Combining type-based analysis and model
checking for finding counterexamples against non-interference. In: PLAS (2006)
59. Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses.
In: CAV (2017)60. Urban, C.: The abstract domain of segmented ranking functions. In: SAS (2013)
61. Urban, C., Miné, A.: An abstract domain to infer ordinal-valued ranking functions.
In: ESOP (2014)62. Volpano, D.M., Irvine, C., Smith, G.: A sound type system for secure flow analysis.
J. Comp. Sec. 4(2-3) (1996)
63. Volpano, D.M., Smith, G.: Eliminating covert flows with minimum typings. In:
CSFW (1997)
64. Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the crossproduct. In: FM (2008)
65. Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: PLDI (2018)
66. Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: ICFP (2015)

24

A

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

The encoding of TI-NI verification from Example 1

inv(Ve1 , Ve2 ) ⇐ x1 = x2 ∧y1 = 0 ∧ (h1 ∧ z1 = 2 × x1 ∨ ¬h1 ∧ z1 = x1 ) ∧y2 = 0 ∧ (h2 ∧ z2 = 2 × x2 ∨ ¬h2 ∧ z2 = x2 )inv(Ve10 , Ve2 ) ⇐ inv(Ve1 , Ve2 ) ∧ schTF (Ve1 , Ve2 ) ∧(z1 > 0 ∧ z10 = z1 − 1 ∧ y10 = y1 + x1 ∨ z1 ≤ 0 ∧ z10 = z1 ∧ y10 = y1 )inv(Ve1 , Ve20 ) ⇐ inv(Ve1 , Ve2 ) ∧ schFT (Ve1 , Ve2 ) ∧(z2 > 0 ∧ z20 = z2 − 1 ∧ y20 = y2 + x2 ∨ z2 ≤ 0 ∧ z20 = z2 ∧ y20 = y2 )0 e0einv(V1 , V2 ) ⇐ inv(Ve1 , Ve2 ) ∧ schTT (Ve1 , Ve2 ) ∧(z1 > 0 ∧ z10 = z1 − 1 ∧ y10 = y1 + x1 ∨ z1 ≤ 0 ∧ z10 = z1 ∧ y10 = y1 ) ∧(z2 > 0 ∧ z20 = z2 − 1 ∧ y20 = y2 + x2 ∨ z2 ≤ 0 ∧ z20 = z2 ∧ y20 = y2 )z1 > 0 ⇐ inv(Ve1 , Ve2 ) ∧ schTF (Ve1 , Ve2 ) ∧ z2 > 0
z2 > 0 ⇐ inv(Ve1 , Ve2 ) ∧ schFT (Ve1 , Ve2 ) ∧ z1 > 0
schTF (Ve1 , Ve2 ) ∨ schFT (Ve1 , Ve2 ) ∨ schTT (Ve1 , Ve2 ) ⇐ inv(Ve1 , Ve2 ) ∧ (z1 > 0 ∨ z2 > 0)
y10 = y20 ⇐ inv(Ve1 , Ve2 ) ∧ z1 ≤ 0 ∧ z2 ≤ 0 ∧(h1 ∧ y10 = y1 ∨ ¬h1 ∧ y10 = 2 × y1 ) ∧(h2 ∧ y20 = y2 ∨ ¬h2 ∧ y20 = 2 × y2 )where Ve1 = x1 , y1 , z1 , h1 , Ve10 = x1 , y10 , z10 , h01 , Ve2 = x2 , y2 , z2 , h2 , Ve20 = x2 , y20 , z20 , h02 ,TF = {1}, FT = {2}, and TT = {1, 2}.

B

The PCSat generated solution of Example 1







x1 = x2 ∧ y1 = y2 ∧ z1 = z2 ∨ ¬h1 ∧ ¬h2 ∧  x2 + y2 = 0 ∧ z1 < 0 ∧

∨





 1 + 2 · x2 = 2 · z2 ∧ 2 + y1 = y2 x1 = x2 ∧ 1 + 2 · x1 6= z2 ∧ 2 · y1 = y2 ∧ 2 · z1 = z2 ∨ ¬h1 ∧ h2 ∧  x1 = x2 ∧ 2 · x1 6= z2 ∧ z1 ≥ 1 ∧ z2 ≥ 1 ∧∨
inv(Ve1 , Ve2 ) ≡  x1 + 2 · y1 = y2 ∧ 2 · z1 = 1 + z2
x1 = x2 ∧ y1 = 2 · y2 ∧ z1 = 2 · z2 ∨
 h1 ∧ ¬h2 ∧  x1 = x2 ∧ 2 · x1 6= z1 ∧ z1 ≥ 1 ∧ z2 ≥ 1 ∧  ∨





y1 = x2 + 2 · y2 ∧ 1 + z1 = 2 · z2
h1 ∧ h2 ∧ x1 = x2 ∧ y1 = y2 ∧ z2 = z2

Constraint-based Relational Verification

C

25

The encoding of the co-termination verification from
Example 2

inv(0, b, Ve1 , Ve2 ) ⇐ fnb(Ve1 , Ve2 , b) ∧ x1 = x2 ∧ y1 = y2
inv(d0 , b, Ve10 , Ve2 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schTF (d, b, Ve1 , Ve2 ) ∧(x1 > 0 ∧ x01 = x1 − y1 ∨ x1 ≤ 0 ∧ x01 = x1 ) ∧(x1 ≤ 0 ∨ x2 ≤ 0 ∨ d0 = d + 1)
inv(d0 , b, Ve1 , Ve20 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schFT (d, b, Ve1 , Ve2 ) ∧(x2 > 0 ∧ x02 = x2 − 2 · y2 ∨ x2 ≤ 0 ∧ x02 = x2 ) ∧(x1 ≤ 0 ∨ x2 ≤ 0 ∨ d0 = d − 1)0 e0einv(d, b, V1 , V2 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schTT (d, b, Ve1 , Ve2 ) ∧(x1 > 0 ∧ x01 = x1 − y1 ∨ x1 ≤ 0 ∧ x01 = x1 ) ∧(x2 > 0 ∧ x02 = x2 − 2 · y2 ∨ x2 ≤ 0 ∧ x02 = x2 )x1 > 0 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schTF (d, b, Ve1 , Ve2 ) ∧ x2 > 0
x2 > 0 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schFT (d, b, Ve1 , Ve2 ) ∧ x1 > 0ee
schTF (d, b, V1 , V2 ) ∨ schFT (d, b, Ve1 , Ve2 ) ∨ schTT (d, b, Ve1 , Ve2 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ (x1 > 0 ∨ x2 > 0)−b ≤ d ∧ d ≤ b ∧ b ≥ 0 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ x1 > 0 ∧ x2 > 0
wfr1 (Ve1 , Ve10 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ x2 ≤ 0 ∧ x1 > 0 ∧ x01 = x1 − y1
wfr2 (Ve2 , Ve20 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ x1 ≤ 0 ∧ x2 > 0 ∧ x02 = x2 − 2 · y2
where Ve1 = x1 , y1 , Ve10 = x01 , y1 , Ve2 = x2 , y2 , Ve20 = x02 , y2 , TF = {1}, FT = {2},and TT = {1, 2}.

D

The PCSat generated solution of Example 2

fnb(x1 , y1 , x2 , u2 , b) ≡ b = 1
x1 = x2 ∧ y1 = y2 ∨inv(d, b, x1 , y1 , x2 , y2 ) ≡ d = 0 ∧ b ≥ 0 ∧ b ≤ 1 ∧y1 = y2 ∧ x1 + y1 ≥ 1 ∧ x2 +2 · y2 ≥ 1
x − 1 ≥ 0 ∧ x − 1 > x0 − 1 ∧ ((x0 > 0 ∧ y 0 ≤ 0) ⇒ x − 1 ≥ 0 ∧ x − 1 > 1 − y 0 ) ∨ 
wfr1 (x, y, x0 , y 0 ) ≡  (x > 0 ∧ y ≤ 0) ∧ 1 − y ≥ 0 ∧ 1 − y > x0 − 1 ∧000 ((x0 > 0 ∧ y0 ≤ 0) ⇒0 1 − y ≥ 0 ∧ 1 − y > 1 − y )(y ≥ 0 ∨ x > 0 ∧ y ≥ 0) ∧
 (y ≥ 0 ∧ (y 0 ≥ 0 ⇒ −y ≥ 0 ∧ −y > −y 0 ) ∧

 0

0
0
0 0


wfr2 (x, y, x , y ) ≡  (x > 0 ∧ y ≥ 0) ⇒ −y ≥ 0 ∧ −y > x ) ∨  (x > 0 ∧ y ≥ 0) ∧ (y 0 ≥ 0 ⇒ x ≥ 0 ∧ x > −y 0 ) ∧  ((x0 > 0 ∧ y 0 ≥ 0) ⇒ x ≥ 0 ∧ x > x0 )Here, wfr1 is induced by the ranking function max(x − 1, if x > 0 ∧ y ≤0 then 1−y else −∞) and wfr2 is induced by the ranking function max(if y ≥0 then − y else − ∞, if x > 0 ∧ y ≥ 0 then x else − ∞).

26

E

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

The encoding of the TS-GNI verification from
Example 3

inv(0, b, Ve1 , Ve2 ) ⇐ fnb(x1 , h1 , l1 , x2 , h2 , l2 , b) ∧ b1 ∧ b2 ∧ l1 = l2 ∧(h1 ∧ x1 = n1 ∨ ¬h1 ∧ x1 = l1 ) ∧(h2 ∧ fnr(p, h2 , l2 , x2 ) ∨ ¬h2 ∧ x2 = l2 )00 eeinv(d , b, V1 , V2 ) ⇐ inv(d,b, Ve1 , Ve2 ) ∧ schTF (d, b, Ve1 , Ve2 ) ∧
b1 ∧ h1 ∧ (x1 ≥ l1 ∧ ¬b01 ∧ x01 = x1 ∨ x1 < l1 ∧ b01 ∧ x01 = x1 ) ∨ ∧ b1 ∧ ¬h1 ∧ (b01 ∧ x01 = x1 + 1 ∨ ¬b01 ∧ x01 = x1 ) ∨00¬b1 ∧ ¬b1 ∧ x1 = x1(¬b1 ∨ ¬b2 ∨ d0 = d + 1)
inv(d0 , b, Ve1 , Ve20 ) ∨ inv(d0 , b, Ve1 , Ve200 ) ⇐ inv(d,b, Ve1 , Ve2 ) ∧ schFT (d, b, Ve1 , Ve2 ) ∧ 
x2 ≥ l2 ∧ ¬b02 ∧ x02 = x2 ∧ ¬b002 ∧ x002 = x2 ∨
b
∧
h
∧
∨
2
 2
x2 < l2 ∧ b02 ∧ x02 = x2 ∧ b002 ∧ x02 = x2
 ∧
 b2 ∧ ¬h2 ∧ (b02 ∧ x02 = x2 + 1 ∧ ¬b002 ∧ x002 = x2 ) ∨

0
0
00
00
¬b2 ∧ ¬b2 ∧ x2 = x2 ∧ ¬b2 ∧ x2 = x2(¬b1 ∨ ¬b2 ∨ d0 = d − 1)inv(d, b, Ve10 , Ve20 ) ∨ inv(d, b, Ve10 , Ve200 ) ⇐ inv(d,b, Ve1 , Ve2 ) ∧ schTT (d, b, Ve1 , Ve2 ) ∧
b1 ∧ h1 ∧ (x1 ≥ l1 ∧ ¬b01 ∧ x01 = x1 ∨ x1 < l1 ∧ b01 ∧ x01 = x1 ) ∨ b1 ∧ ¬h1 ∧ (b01 ∧ x01 = x1 + 1 ∨ ¬b01 ∧ x01 = x1 ) ∨
 ∧
0
0
¬b
∧
¬b
∧
x
=
x
1
1
1 1

 
x2 ≥ l2 ∧ ¬b02 ∧ x02 = x2 ∧ ¬b002 ∧ x002 = x2 ∨∨ b2 ∧ h2 ∧ x2 < l2 ∧ b02 ∧ x02 = x2 ∧ b002 ∧ x02 = x2


0
0
00
00
 b2 ∧ ¬h2 ∧ (b2 ∧ x2 = x2 + 1 ∧ ¬b2 ∧ x2 = x2 ) ∨¬b2 ∧ ¬b02 ∧ x02 = x2 ∧ ¬b002 ∧ x002 = x2
b1 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schTF (d, b, Ve1 , Ve2 ) ∧ b2
b2 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ schFT (d, b, Ve1 , Ve2 ) ∧ b1eee
schTF (d, b, V1 , V2 ) ∨ schFT (d, b, V1 , Ve2 ) ∨ schTT (d, b, Ve1 , Ve2 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ (b1 ∨ b2 )−b ≤ d ∧ d ≤ b ∧ b ≥ 0 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ b1 ∧ b2
x1 = x2 ⇐ inv(d, b, Ve1 , Ve2 ) ∧ ¬b1 ∧ ¬b2 ∧ p = x1
wfr(Ve2 , Ve20 ) ⇐ inv(d, b, Ve1 , Ve2 ) ∧ ¬b1 ∧ p = x1 ∧ b2 ∧ h2 ∧ x2 < l2 ∧ x02 = x2

where Ve1 = p, b1 , x1 , h1 , l1 , Ve10 = p, b01 , x01 , h1 , l1 , Ve2 = b2 , x2 , h2 , l2 , Ve20 = b02 , x02 , h2 , l2 ,Ve200 = b002 , x002 , h2 , l2 , TF = {1}, FT = {2}, and TT = {1, 2}.

Constraint-based Relational Verification

F

27

The PCSat generated solution of Example 3

fnb(x1 , y1 , x2 , u2 , b) ≡ b = 0
fnr(p, h2 , l2 , x2 ) ≡ 
x2 = p¬h1 ∧ ¬h2 ∧ d = 0 ∧ b = 0 ∧ b2 ∧ x2 ≥ l2 ∧ l1 = l2 ∨ ¬h1 ∧ h2 ∧ d = 0 ∧ b ≥ 0 ∧ x1 ≥ l1 ∧ p = x2 ∧ l1 = l2 ∨


 


d = 0 ∧ b = 0 ∧ b2 ∧ l1 = l2 ∨


e
e



∨
inv(d, b, V1 , V2 ) ≡  h1 ∧ ¬h2 ∧ l1 = x2 ∧ p = x1 ∧ x1 ≥ l1 ∧ d ≥ 1 + b∧





 b = l2 ∧ 1 + 2 · x 1 + 2 · x 2 = 0
d = 0 ∧ b = 0 ∧ b1 ∧ l 1 = l 2 ∧ x 2 = p ∨h1 ∧ h2 ∧¬b1 ∧ x1 ≥ l1 ∧ p = x2 ∧ l1 = l2
wfr(x, h, l, x0 , h0 , l0 ) ≡ ¬h ∧ l − x ≥ 0 ∧ l − x > l0 − x0 ∨ h ∧ x ≥ 0 ∧ x > x0
where Ve1 = p, b1 , x1 , h1 , l1 and Ve2 = b2 , x2 , h2 , l2 .

G

Proof of Theorem 1

Proof:(only-if )The only-if direction holds from the completeness of the standard lock-step
product program construction that executes each programs synchronously
in parallel. That is, such a product program is realized by the the scheduler
defined by sch[k] = true and schA = false for all A 6= [k]. Note that clauses(4) and (5) are trivially satisfied by such a scheduler. The corresponding
inv is the set of tuples of states reachable by the lock-step evaluation fromthe tuples of states satisfying Pre (or any invariant used to verify the input
instance under the lock-step product program construction). It is easy to seethat such inv satisfies the rest of the clauses with the scheduler. (A similarargument can also be made with the standard sequential product program
construction.)(if )We prove the if direction by proving the contrapositive. So, suppose thatthe tuple of programs violates the k-safety property. Then, there must be
sequences π1 , . . . , πk such that (a) Pre(π1 [1], . . . , πk [1]) is true, (b) for each
πi , Fi (πi [|πi |]) is true, (c) ¬Post(π1 [|π1 |], . . . , πk [|πk |]) is true, and (d) for
each πi and 1 < j ≤ |πi |, Ti (πi [j − 1], πi [j]) is true. The following argument, roughly, says that under any scheduler satisfying CS , we can “reach”
π1 [|π1 |], . . . , πk [|πk |] from π1 [1], . . . , πk [1]. Let ai = 1 for each i ∈ [k]. Let
ve = π1 [a1 ], . . . , πk [ak ]. By (a) and clause (1), it must be the case that inv(ev)
is true.
If all programs have terminated (i.e., Fi (πi [ai ]) for each i), then by (b), (c)and the fact that programs self-loop after reaching final states, ve invalidates
clause (3) and therefore we have shown that
W CS is unsatisfiable. So, supposethat there are unfinished programs (i.e., i∈[k] ¬Fi (πi [ai ]) is true). By clause

28

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen(5), there must be some A ∈ P + [k] such that schA (ev ) is true. Then, by clause(4), there must be unfinished programs that A schedules to be evaluated next,that is, B = {i ∈ A | ¬Fi (πi [ai ])} is non-empty. Let a0i = ai + 1 if i ∈ B andotherwise let a0i = ai . Let ve0 = π1 [a01 ], . . . , πk [a0k ]. Then, inv(ev 0 ) must be trueby (d) and clause (2).
Repeating the argument in the above paragraph by setting ve to ve0 andai to a0i for each i ∈ [k], we will eventually reach the terminal tuple of states
π1 [|π1 |], . . . , πk [|πk |] and show that inv(π1 [|π1 |], . . . , πk [|πk |]) must be true,
which, by (c), invalidates clause (3) and therefore CS is unsatisfiable.


H

Proof of Theorem 2

Proof:(only-if )Suppose that given pair of programs co-terminate. Let schTT = true andschFT = schTF = false, i.e., let the scheduler be lock-step. Let fnb(Ve , b) =b = 0 (any other predicate that sets b to be non-negative also works). Let
inv be the set of tuples (d, 0, ve1 , ve2 ) where ve1 , ve2 are the tuples of states
reachable from Pre by lock-step evaluation and d = 0 if ¬F1 (ve1 ) ∧ ¬F2 (ve2 )(d is arbitrary if F1 (ve1 ) ∨ F2 (ve2 )). Let R be the set of states of P2 reachable
from a pair of states satisfying Pre after the corresponding execution of P1
has terminated by lock-step evaluation. That is, R is the set of states ve2
satisfying the following: there exist a pair of states (ve1 0 , ve2 0 ) and a state ve1
such that Pre(ve1 0 , ve2 0 ) is true, (ve1 , ve2 ) is reachable from (ve1 0 , ve2 0 ) by lock-stepevaluation, and F1 (ve1 ) is true. Let wfr = (R × R) ∩ {(ev , ve0 ) | T2 (ev , ve0 )} (orany other well-founded relation witnessing the termination of R). It is easy
to see that these predicates satisfy CCoT .
(if )We prove the if direction by proving the contrapositive. So, suppose that thepair of programs violates co-termination. Then, there must be states ve1 ,ve2 ,and ve1 0 such that Pre(ve1 , ve2 ) is true, ve1 1 ve1 0 , and ve2 2 ⊥. Let π1 bea finite sequence such that (a1) ve1 = π1 [1], (b1) F1 (π1 [|π1 |]) is true, and(c1) for each 1 < i ≤ |π1 |, T1 (π1 [i − 1], π1 [i]) is true. Let $2 be an infinite
sequence such that (a2) ve2 = $2 [1], (b2) for each i ≥ 1, F2 ($2 [i]) is false,and (c2) for each i > 1, T2 ($2 [i − 1], $2 [i]) is true.
Let c ∈ Z be such that fnb(π1 [1], $2 [1], c) is true. By clause (1), it must
be the case that inv(0, c, π1 [1], $2 [1]) is true. We next show the following
lemma.
Lemma 1. Let d ∈ Z, 1 ≤ i ≤ |π1 |, and 1 ≤ j. Suppose inv(d, c, π1 [i], $2 [j])and F1 (π1 [i]). Then, clauses (6), (5), (4a), (4b), (3a), (3c) cannot be simultaneously satisfied.

Constraint-based Relational Verification

29

Proof: By F1 (π1 [i]), (4a), (4b), and (5), we have that schTT (d, c, π1 [i], $2 [j])or schFT (d, c, π1 [i], $2 [j]) must be true. In either case, by (c2), (3a), (3c) andthe fact that T1 (π1 [i], π1 [i]), inv(d0 , b, π1 [i], $2 [j + 1]) must be true for somed0 ∈ Z (incidentally, d0 = d + 1 or d0 = d). Also, by F1 (π1 [i]) and (6b),wfr($2 [j], $2 [j + 1]) is true.
Repeating the above argument with j updated to j + 1 and d updated tod0 , we derive that wfr($1 [j 0 ], $2 [j 0 + 1]) must be true for all j 0 ≥ j. However,this violates the condition that wfr is a well-founded relation. Therefore, theclauses cannot be satisfied.

We now return to the proof of the theorem. Let d = 0, a1 = 1 and a2 = 1.
Note that inv(d, c, π1 [a1 ], $2 [a2 ]) is true and |d| ≤ c.
If F1 (π1 [a1 ]) is true, then by Lemma 1, the constraint is unsatisfiable.
So, suppose that ¬F1 (π1 [a1 ]). By clause (5), it must be the case that either(sTT ) schTT (d, c, π1 [a1 ], $2 [a2 ]) is true;(sTF ) schTF (d, c, π1 [a1 ], $2 [a2 ]) is true; or(sFT ) schFT (d, c, π1 [a1 ], $2 [a2 ]) is true.
If (sTT ) then let d0 = d, a01 = a1 + 1, and a02 = a2 + 1. If (sFT ) then let
d0 = d − 1, a01 = a1 , and a02 = a2 + 1. If (sTF then let d0 = d + 1, a01 = a1 , and
a02 = a2 +1. In any case, by (b2), (3a), (3b), and (3c), inv(d0 , c, π1 [a01 ], $2 [a02 ])must be true. But by (b2) and (2), it must be the case that |d0 | ≤ c.
Repeating the argument in the above paragraph by setting d = d0 , a1 =0
a1 , and a2 = a02 , we will eventually reach a1 = |π1 | such that inv(d, c, π1 [a1 ], $2 [a2 ])is true for some d and a2 , because schFT can only become true finitely often
due to the difference bound. At this point, F1 (π1 [a1 ]) is true. Therefore by
Lemma 1, the constraint is unsatisfiable.
I

Proof of Theorem 3

Proof:(if )Suppose that ρ is a solution to CT IGN I . Let P20 be a program whose transition
relation T20 is defined as follows:
T20 = {(ev , ve2 , ve, ve2 0 ) | ∃r.ρ(fnr)(ev , ve2 , r) ∧ U2 (r, ve2 , ve2 0 )}f1 | and fnr is the functional predicate variable added in (m6) of
where |ev | = |VDef. 7. That is, P20 is P2 augmented to (1) take prophecy values as input andpropagate them across the transitions, and (2) determinize the transitions
by the assignment to fnr given in ρ. We write 02 for the reachability relationof P20 .99The encoding given in Sec. 4.3 modified P1 to propagate the prophecy values. Here,
we modify P2 for the job. The resulting constraint set is equivalent, but the proof
becomes somewhat simpler.

30

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
0f2 , r)
Let CTIGNI
be CTIGNI but modified so that its occurrences of fnr(ep, V00f2 , r). Clearly, ρ is a solution to C
are replaced by ρ(fnr)(ep, V
TIGNI . Also, CTIGNI
is a k-safety constraint set (cf. Def. 3) for P1 and P20 against the pre-condition
Pre 0 and the post-condition Post 0 . Therefore, by Theorem 1, P1 and P20
satisfies the k-safety property given by Pre 0 and Post 0 .
0Now, suppose that Pre(ve1 , ve2 ) and ve1
e be valuations of1 ve1 . Let v
prophecy variables (i.e., |ev | = |ve1 |). We have Pre 0 (ev , ve1 , ve2 ). Also, by ksafety of P1 and P20 , either (a) (ev , ve2 ) 02 ⊥ or (b) there exists ve2 0 such that000(ev , ve2 ) 2 (ev , ve2 ) and Post (ev , ve1 0 , ve2 0 ).
If the former is true for some ve, then we have ve2 2 ⊥ by letting P2 resolve the non-deterministic choices according to the execution (ev , ve2 ) 02 ⊥.
0
Otherwise, (b) holds for all ve. Therefore, there exists ve2 such that (ve1 , ve2 ) 02
(ve1 , ve2 0 ) and Post 0 (ve1 , ve1 0 , ve2 0 ). Therefore, by letting P2 resolve the non00
deterministic choices according to the execution (ve1 , ve2 )2 (ve1 , ve2 ), we000
have ve2
2 ve2 and Post(ve1 , ve2 ). Therefore, P1 and P2 satisfies TI-GNI
given by Pre and Post.

(only-if )Suppose that P1 and P2 satisfy TI-GNI given by Pre and Post. Let us write
π : ve i ve0 if π is a finite sequence witnessing the reachability relationve i ve0 . Likewise, let us write $ : ve i ⊥ if $ is an infinite sequencewitnessing the non-termination ve i ⊥.
For each state ve1 0 of P1 , we define L(ve1 0 ) to be a (possibly infinite) listof finite and infinite sequences obtained by totally ordering the elements ofthe following set:
{π | ∃ve1 , ve2 , ve1 0 ve2 0 .Pre(ve1 , ve2 ) ∧ ve1 1 ve1 0 ∧ π : ve2 2 ve2 0 ∧ Post(ve1 0 , ve2 0 )} ∪{$ | ∃ve1 , ve2 , ve1 0 .Pre(ve1 , ve2 ) ∧ ve1 1 ve1 0 ∧ $ : ve2 2 ⊥}That is, L(ve1 0 ) is a list of the terminating and non-terminating execution
traces of P2 that can match a (terminating) execution trace of P1 whose
final state is ve1 0 . Note that, if Pre(ve1 , ve2 ) and v1 1 ve1 0 , then there existsξ ∈ L(ve1 0 ) such that ξ[1] = ve2 .
For ξ ∈ L(ve1 0 ) and 1 ≤ i ≤ |ξ| (where |$| = ∞ for an infinite trace$), let choice(ξ, i) be the angelic non-deterministic choice made in the i-th
step of the execution ξ. For a function f , we write f [a 7→ b] for the function
defined by f [a 7→ b](a) = b and f [a 7→ b](c) = f (c) for all c 6= a.
Next, we define a function det by the following process. Initialize det ← ∅.
Then, for each state ve1 0 of P1 , apply the steps below until L(ve1 0 ) is empty:
1. Take the head element ξ ∈ L(ve1 0 ).
2. Scan ξ forwards and, at each position i, record its angelic choice by
updating det ← det[(ve1 0 , ξ[i]) 7→ choice(ξ, i)] if (ve1 0 , ξ[i]) ∈/ dom(det)and otherwise leave det unchanged.
Finally, for each pair (ve1 , ve2 ) of states of P1 and and P2 such that (ve1 , ve2 ) ∈/dom(det), update det by setting det ← det[(ve1 , ve2 ) 7→ r] where r is arbitrary.
Note that this is an infinite “process” in general since the number of states ofConstraint-based Relational Verification

31

P1 , |L(ve1 0 )|, and the length of a sequence in L(ve1 0 ), can all be infinite. However, it is well-defined. Importantly, det thus constructed is a total function
from the pairs of P1 and P2 states.
Note that using det as the determinizing choice function in P20 would
make P1 and P20 (cf. the soundness proof above) satisfy the k-safety property
given by Pre 0 and Post 0 . This follows from the fact that, if Pre(ve1 , ve2 ) andve1 1 ve1 0 , then any execution of P20 from (ve1 0 , ve2 ) only visits states (ve1 0 , ve)
where ve occurs in L(ve1 0 ) and therefore may only reach an output (ve1 0 , ve2 0 )such that Post(ve1 0 , ve2 0 ) is true.10
Therefore, the rest of the proof follows the structure of the completenessdirection of the proof of Theorem 1. Let us call a pair of states ve1 and (ve1 0 , ve2 )of P1 and P20 initial if Pre 0 (ve1 0 , ve1 , ve2 ) is true (i.e., Pre(ve1 , ve2 ) is true). Also,in what follows, we assume that P20 uses det as the determinizing choicefunction.
Let schTT = true and schFT = schTF = false, i.e., let the scheduler belock-step. Let fnr be the set of tuples (ve1 0 , ve2 , r) such that det(ve1 0 , ve2 ) =r, i.e., fnr expresses the graph of det. Note that fnr trivially satisfies thefunction-ness requirement. Let inv be the set of tuples (ve1 0 , ve1 , ve2 ) where ve1and (ve1 0 , ve2 ) are pair of states of P1 and P20 reachable from some initial pairof states by lock-step evaluation. It is easy to see that these predicates satisfy
CTIGNI .


J

Proof of Theorem 4

Proof:(if )The proof is similar to the soundness direction of Theorem 3 and proceeds
by determinizing P2 using the solution to the constraint set. So, suppose that
ρ is a solution to CT SGN I . Let P20 be a program whose transition relation T20
is defined as follows:
T20 = {(ev , ve2 , r) ∧ U2 (r, ve2 , ve2 0 )}v , ve2 , ve, ve2 0 ) | ∃r.ρ(fnr)(ef1 | and fnr is the functional predicate variable added in (m6) of
where |ev | = |VDef. 7. That is, P20 is P2 augmented to (1) take prophecy values as input andpropagate them across the transitions, and (2) determinize the transitions by
the assignment to fnr given in ρ. We write 02 for the reachability relation of
P20 . We also consider modification of P1 , P10 , that is defined by the transition
relation T10 and the final state predicate F10 given in Def. 8. We write 01 for
10

However, the behavior of P20 is not necessarily equivalent to what the traces inL(ve1 0 ) stipulate. For instance, P20 may non-terminate even when all traces in L(ve1 0 )are finite.

32

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen

the reachability relation of P10 . Note that, propagating the prophecy values
in both P10 and P20 is equivalent to propagating them in one of the two, sinceneither transitions modify the prophecy values.
0f2 , r)
Let CTSGNIbe CTSGNI but modified so that its occurrences of fnr(ep, V0f2 , r). Clearly, ρ is a solution to C
are replaced by ρ(fnr)(ep, V
TSGNI . Note that0
CTSGNI
asserts a conjunction of the k-safety for P10 and P20 against the precondition Pre 0 and the post-condition Post 0 and the co-termination for P10
and P20 against the pre-condition Pre 0 . Therefore, by Theorem 1, (a) P10 andP20 satisfies the k-safety property given by Pre 0 and Post 0 , and by Theorem 2,(b) P10 and P20 satisfies the co-termination property given by Pre 0 .
Now, suppose that Pre(ve1 , ve2 ) and ve1 1 ve1 0 . We have Pre 0 (ve1 , ve1 , ve2 )and (ve1 , ve1 ) 01 (ve1 , ve1 0 ). Therefore, by (b), we have that (ve1 , ve2 ) 6 02 ⊥.
Therefore, (ve1 , ve2 ) 02 (ve1 , ve2 0 ) for some ve2 0 , assuming that every pre-related
state has at least one execution. Then, by (a), it must be the case that
Post 0 (ve1 , ve1 0 , ve2 0 ). Therefore, by letting P2 resolve the non-deterministic choices000
according to the execution (ve1 , ve2 )2 ve2 and2 (ve1 , ve2 ), we have ve200
Post(ve1 , ve2 ). Therefore, P1 and P2 satisfies TS-GNI given by Pre and Post.
(only-if )The proof is similar to the completeness direction of Theorem 3 and proceedsby constructing a determinizing choice function F from the executions of thetwo programs. We will use some of the notations defined there. That is, wewrite π : ve i ve0 if π is a finite sequence witnessing the reachability relationve i ve0 , and when π is an execution of P2 and 1 ≤ i ≤ |π|, we write
choice(π, i) be the angelic non-deterministic choice made in the i-th stepof π. Also, for a function f , we write f [a 7→ b] for the function defined byf [a 7→ b](a) = b and f [a 7→ b](c) = f (c) for all c 6= a.
Now we proceed with the proof of the completeness direction. So, supposethat P1 and P2 satisfy TI-GNI given by Pre and Post. For each state ve1 0 of
P1 , we define L(ve1 0 ) to be a (possibly infinite) list of finite sequences obtainedby totally ordering the elements of the following set:
{π | ∃ve1 , ve2 , ve1 0 ve2 0 .Pre(ve1 , ve2 ) ∧ ve1

1 ve1

0

∧ π : ve2

2 ve2

0

∧ Post(ve1 0 , ve2 0 )}That is, L(ve1 0 ) is a list of the terminating execution traces of P2 that canmatch a (terminating) execution trace of P1 whose final state is ve1 0 . Note
that, if Pre(ve1 , ve2 ) and v1 1 ve1 0 , then there exists π ∈ L(ve1 0 ) such that
π[1] = ve2 .
Next, we define a function det by the following process. Initialize det ← ∅.
Then, for each state ve1 0 of P1 , apply the steps below until L(ve1 0 ) is empty:
1. Take the head element π ∈ L(ve1 0 ).
2. Scan π forwards and, at each position i, record its angelic choice by
updating det ← det[(ve1 0 , π[i]) 7→ choice(π, i)].
Finally, for each pair (ve1 , ve2 ) of states of P1 and and P2 such that (ve1 , ve2 ) ∈/dom(det), update det by setting det ← det[(ve1 , ve2 ) 7→ r] where r is arbitrary.
As that in the proof of Theorem 3, this is an infinite “process” in general

Constraint-based Relational Verification

33

since the number of states of P1 and |L(ve1 0 )| can both be infinite. However,
it is well-defined. Importantly, det thus constructed is a total function fromthe pairs of P1 and P2 states.
An important difference from the construction of det given in Theorem 3
is that in step 2., we always update det by the angelic choice, i.e., even if(ve1 0 , ξ[i]) ∈ dom(det). This ensures the “co-termination” of P20 when it isdeterminized by det.11
Note that using det as the determinizing choice function in P20 would
make P10 and P20 (cf. the soundness proof above) satisfy the k-safety property
given by Pre 0 and Post 0 and the co-termination property given by Pre 0 . This
follows from the fact that, if Pre(ve1 , ve2 ) and ve1 1 ve1 0 , then any executionof P20 from (ve1 0 , ve2 ) only visits states (ve1 0 , ve) where ve occurs in L(ve1 0 ) andreaches an output (ve1 0 , ve2 0 ) such that Post(ve1 0 , ve2 0 ) is true. In particular, thetermination of P20 from such a state (ve1 0 , ve2 ) is guaranteed by the fact that
all traces in L(ve1 0 ) are finite.
Therefore, the rest of the proof follows the structures of the completenessdirections of the proofs of Theorems 1 and 2. Let us call a pair of states(ve1 0 , ve1 ) and (ve1 0 , ve2 ) of P10 and P20 initial if Pre 0 (ve1 0 , ve1 , ve2 ) is true (i.e.,Pre(ve1 , ve2 ) is true). Also, in what follows, we assume that P20 uses det as thedeterminizing choice function.
Let schTT = true and schFT = schTF = false, i.e., let the scheduler belock-step. Let fnr be the set of tuples (ve1 0 , ve2 , r) such that F (ve1 0 , ve2 ) = r, i.e.,
fnr expresses the graph of F . Note that fnr trivially satisfies the functionness requirement. Let fnb(Ve , b) = b = 0 (any other predicate that sets b
to be non-negative also works). Let inv be the set of tuples (d, 0, ve1 0 , ve1 , ve2 )where ve1 0 , ve1 and (ve1 0 , ve2 ) are reachable from some initial pair of states bylock-step evaluation, and d = 0 if ¬F10 (ve1 0 , ve1 ) ∧ ¬F20 (ve1 0 , ve2 ) (d is arbitrary if
F10 (ve1 0 , ve1 )∨F20 (ve1 0 , ve2 )). Let R be the set of states of P20 reachable from some
initial pair of states after the corresponding execution of P10 has terminatedby lock-step evaluation. That is, R is the set of states (ve1 0 , ve2 ) satisfying thefollowing: there exist a state (ve1 0 , ve1 ) such that ((ve1 0 , ve1 ), (ve1 0 , ve2 )) is reachable from some initial pair of states by lock-step evaluation and F10 (ve1 0 , ve1 )is true. Let wfr = (R × R) ∩ {((ve1 0 , ve2 ), (ve1 0 , ve2 0 )) | T20 ((ve1 0 , ve2 ), (ve1 0 , ve2 0 ))} (orany other well-founded relation witnessing the termination of R). It is easy
to see that these predicates satisfy CTSGNI .


K

Unsatisfiability Checking of Example Instances

The unsatisfiability of the given example instances (E, K) can be decided by an
off-the-shelf SAT solver if E has only ordinary predicate variables because E is a
finite set of clauses not containing term variables. Otherwise, we use the following
11

The above “overwriting” construction of det actually also works for the proof of Theorem 3. However, the construction method given there does not work here because
it may introduce unwanted non-termination.

34

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen(CDCL-like) iterative algorithm staring from E0 = E: For each iteration i ≥ 0,
we first check whether (Ei , ∅) is unsatisfiable. If so, then we conclude that (E, K)
is unsatisfiable. Otherwise, we obtain a satisfying assignment σ for Ei . Then, foreach well-founded predicate variable X, we consider the graph comprising theedges { (ev1 , ve2 ) | |= σ(X(ev1 , ve2 )) } and enumerate its simple cycles (e.g., by using
the algorithm of [35]). Note that such cycles would be counterexamples to thewell-foundedness constraint X. Also, for each functional predicate variable X, weenumerate the pairs {X(ev , v1 ), X(ev , v2 )} such that v1 6= v2 and |= σ(X(ev , v1 ) ∧X(ev , v2 )), which would be counterexamples to the functionality constraint X. If
no such cycles nor pairs exist, we conclude that (E, K) is satisfiable. Otherwise,
we let Ei+1 be Ei but with the following new learnt clauses added:– ¬X(ev1 , ve2 ) ∨ · · · ∨ ¬X(evm−1 , vem ) for each simple cycle ve1 , . . . , vem = ve1 ofeach well-founded predicate X, and– ¬X(ev , v1 ) ∨ ¬X(ev , v2 ) for each pair {X(ev , v1 ), X(ev , v2 )} of each functional
predicate X.
We then proceed to the next iteration with Ei+1 .
It is worth mentioning here that if the original pfwCSP (C, K) is unsatisfiable
and C has no well-founded predicate variable, there always exists an unsatisfiable
finite set E of example instances of C. However, there is, in general, no such finite
witness of the unsatifiability if C has a well-founded predicate variable.

L

A Refined Stratified Template Family for Well-Founded
Predicates⇓
The stratified template family TX
for well-founded predicates shown in Fig. 2 canbe further refined without loss of generality by simplifying and using if r(ex) ≥0 then r(ex) else −1 instead of r(e
x).

W

np
⇓
TX
(np, nl , nc, rc, rd , dc, dd ) , λ(ex, ye).
D
(e
y
)
j
j=1
W

Vnp
np
∧
x) ∧ j=1 (Dj (ey ) ⇒ DEC i,j (ex, ye))
i=1 Di (eWnlri,k (ex) ≥ 0 ∧ ri,k (ex) > rj,k (ey )∧DEC i,j (ex, ye) , k=1 Vk−1x) < 0 ∧ rj,` (ey ) < 0 ∨ ri,` (ex) ≥ rj,` (ey ))`=1 (ri,` (eM

Relational Verification Benchmarks

Our relational verification benchmark set consists of:– The k-safety verification problem DoubleSquareNI_h** from Example 1, which
is originally introduced in [51].
– The k-safety verification problem HalfSquareNI of the following program
obtained from [51]:Constraint-based Relational Verification35

pre(low1 == low2)
halfSquare(int h, int low) {assume(low > h > 0);
int i = 0, y = 0, v = 0;
while (h > i) {i++; y += y;}v = 1;
while (low > i) {i++; y += y;}return y;}post(y1 == y2)

The encoded constraints are:Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2) :low1 = low2, low1 > h1, h1 > 0, low2 > h2, h2 > 0,b1, i1 = 0, y1 = 0, v1 = 0,b2, i2 = 0, y2 = 0, v2 = 0.
Inv(b1’ : bool, h1, low1, i1’, y1’, v1’, b2 : bool, h2, low2, i2, y2, v2) :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchTF(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
b1 and h1 > i1 and b1’ and i1’ = i1 + 1 and y1’ = y1 + y1 and v1’ = v1 or
b1 and h1 <= i1 and !b1’ and i1’ = i1 and y1’ = y1 and v1’ = 1 or!b1 and low1 > i1 and !b1’ and i1’ = i1 + 1 and y1’ = y1 + y1 and v1’ = v1 or!b1 and low1 <= i1 and !b1’ and i1’ = i1 and y1’ = y1 and v1’ = v1.
Inv(b1 : bool, h1, low1, i1, y1, v1, b2’ : bool, h2, low2, i2’, y2’, v2’) :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchFT(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),b2 and h2 > i2 and b2’ and i2’ = i2 + 1 and y2’ = y2 + y2 and v2’ = v2 or
b2 and h2 <= i2 and !b2’ and i2’ = i2 and y2’ = y2 and v2’ = 1 or!b2 and low2 > i2 and !b2’ and i2’ = i2 + 1 and y2’ = y2 + y2 and v2’ = v2 or!b2 and low2 <= i2 and !b2’ and i2’ = i2 and y2’ = y2 and v2’ = v2.
Inv(b1’ : bool, h1, low1, i1’, y1’, v1’, b2’ : bool, h2, low2, i2’, y2’, v2’) :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchTT(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
b1 and h1 > i1 and b1’ and i1’ = i1 + 1 and y1’ = y1 + y1 and v1’ = v1 or
b1 and h1 <= i1 and !b1’ and i1’ = i1 and y1’ = y1 and v1’ = 1 or!b1 and low1 > i1 and !b1’ and i1’ = i1 + 1 and y1’ = y1 + y1 and v1’ = v1 or!b1 and low1 <= i1 and !b1’ and i1’ = i1 and y1’ = y1 and v1’ = v1,
b2 and h2 > i2 and b2’ and i2’ = i2 + 1 and y2’ = y2 + y2 and v2’ = v2 or
b2 and h2 <= i2 and !b2’ and i2’ = i2 and y2’ = y2 and v2’ = 1 or!b2 and low2 > i2 and !b2’ and i2’ = i2 + 1 and y2’ = y2 + y2 and v2’ = v2 or36

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen!b2 and low2 <= i2 and !b2’ and i2’ = i2 and y2’ = y2 and v2’ = v2.
b1 or low1 > i1 :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchTF(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),b2 or low2 > i2.
b2 or low2 > i2 :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchFT(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
b1 or low1 > i1.
SchTF(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchFT(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
SchTT(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2) :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
b1 or low1 > i1 or b2 or low2 > i2.
y1 = y2 :Inv(b1 : bool, h1, low1, i1, y1, v1, b2 : bool, h2, low2, i2, y2, v2),
!b1, low1 <= i1, !b2, low2 <= i2.

– The k-safety verification problem ArrayInsert of the following program obtained from [51] by simulating the control flow of the original array-manipulating
program:pre(len1 == len2)
int arrayInsert(int len, int h) {int i=0;
while (i < len && i != h) i++;len = len + 1;
while (i < len) i++;return i;}post(i1 == i2)

The encoded constraints are:Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2) :len1 = len2, b1, i1 = 0, b2, i2 = 0.
Inv(b1’ : bool, len1’, h1, i1’, b2 : bool, len2, h2, i2) :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchTF(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
b1 and i1 < len1 and i1 <> h1 and b1’ and len1’ = len1 and i1’ = i1 + 1 orb1 and (i1 >= len1 or i1 = h1) and !b1’ and len1’ = len1 + 1 and i1’ = i1 or!b1 and i1 < len1 and !b1’ and len1’ = len1 and i1’ = i1 + 1 orConstraint-based Relational Verification37!b1 and i1 >= len1 and !b1’ and len1’ = len1 and i1’ = i1.
Inv(b1 : bool, len1, h1, i1, b2’ : bool, len2’, h2, i2’) :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchFT(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),b2 and i2 < len2 and i2 <> h2 and b2’ and len2’ = len2 and i2’ = i2 + 1 orb2 and (i2 >= len2 or i2 = h2) and !b2’ and len2’ = len2 + 1 and i2’ = i2 or!b2 and i2 < len2 and !b2’ and len2’ = len2 and i2’ = i2 + 1 or!b2 and i2 >= len2 and !b2’ and len2’ = len2 and i2’ = i2.
Inv(b1’ : bool, len1’, h1, i1’, b2’ : bool, len2’, h2, i2’) :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchTT(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
b1 and i1 < len1 and i1 <> h1 and b1’ and len1’ = len1 and i1’ = i1 + 1 orb1 and (i1 >= len1 or i1 = h1) and !b1’ and len1’ = len1 + 1 and i1’ = i1 or!b1 and i1 < len1 and !b1’ and len1’ = len1 and i1’ = i1 + 1 or!b1 and i1 >= len1 and !b1’ and len1’ = len1 and i1’ = i1,b2 and i2 < len2 and i2 <> h2 and b2’ and len2’ = len2 and i2’ = i2 + 1 orb2 and (i2 >= len2 or i2 = h2) and !b2’ and len2’ = len2 + 1 and i2’ = i2 or!b2 and i2 < len2 and !b2’ and len2’ = len2 and i2’ = i2 + 1 or!b2 and i2 >= len2 and !b2’ and len2’ = len2 and i2’ = i2.
b1 or i1 < len1 :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchTF(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),b2 or i2 < len2.
b2 or i2 < len2 :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchFT(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),b1 or i1 < len1.
SchTF(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchFT(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
SchTT(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2) :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),b1 or i1 < len1 or b2 or i2 < len2.
i1 = i2 :Inv(b1 : bool, len1, h1, i1, b2 : bool, len2, h2, i2),
!b1, i1 >= len1, !b2, i2 >= len2.

– The k-safety verification problem SquareSum of the following program obtained from [51] by replacing the nonlinear expression a*a in the original
program with a:pre(a1 < a2 && b2 < b1)
squaresSum(int a, int b) {assume(0 < a < b);
int c=0;

38

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
while (a<b) { c+=a; a++; }return c;}post(c2 < c1)

The encoded constraints are:Inv(a1, b1, c1, a2, b2, c2) :a1 < a2, b2 < b1,
0 < a1, a1 < b1, 0 < a2, a2 < b2,
c1 = 0, c2 = 0.
Inv(a1’, b1, c1’, a2, b2, c2) :Inv(a1, b1, c1, a2, b2, c2),
SchTF(a1, b1, c1, a2, b2, c2),
a1 < b1 and c1’ = c1 + a1 and a1’ = a1 + 1 or a1 >= b1 and c1’ = c1 and a1’ = a1.
Inv(a1, b1, c1, a2’, b2, c2’) :Inv(a1, b1, c1, a2, b2, c2),
SchFT(a1, b1, c1, a2, b2, c2),
a2 < b2 and c2’ = c2 + a2 and a2’ = a2 + 1 or a2 >= b2 and c2’ = c2 and a2’ = a2.
Inv(a1’, b1, c1’, a2’, b2, c2’) :Inv(a1, b1, c1, a2, b2, c2),
SchTT(a1, b1, c1, a2, b2, c2),
a1 < b1 and c1’ = c1 + a1 and a1’ = a1 + 1 or a1 >= b1 and c1’ = c1 and a1’ = a1,
a2 < b2 and c2’ = c2 + a2 and a2’ = a2 + 1 or a2 >= b2 and c2’ = c2 and a2’ = a2.
a1 < b1 :Inv(a1, b1, c1, a2, b2, c2),
SchTF(a1, b1, c1, a2, b2, c2), a2 < b2.
a2 < b2 :Inv(a1, b1, c1, a2, b2, c2),
SchFT(a1, b1, c1, a2, b2, c2), a1 < b1.
SchTF(a1, b1, c1, a2, b2, c2),
SchFT(a1, b1, c1, a2, b2, c2),
SchTT(a1, b1, c1, a2, b2, c2) :Inv(a1, b1, c1, a2, b2, c2),
a1 < b1 or a2 < b2.
c2 < c1 :- Inv(a1, b1, c1, a2, b2, c2), a1 >= b1, a2 >= b2.

In the experiment, we provided the following constraint as a hint:
a1 > 0, b2 < b1 :- Inv(a1, b1, c1, a2, b2, c2).

– The co-termination verification problem CotermIntro from Example 2.

Constraint-based Relational Verification

39– The TS-GNI verification problem TS_GNI_h** from Example 3. In the experiment of TS_GNI_hFT, we provided the following constraint as a hint:x1 >= low1 :- Inv(pr, d, b, b1 : bool, x1, low1, b2 : bool, x2, low2).

In the experiment of TS_GNI_hTT, we provided the following constraint as ahint:
b1 or x1 >= low1 :- Inv(pr, d, b, b1 : bool, x1, low1, b2 : bool, x2, low2).

Note that these are a part of necessary non-relational invariant.
– The TS-GNI verification problem SimpleTS_GNI1 of the following program:
while ( * ) { x ++; }; return (high + x);

The encoded constraints are:Inv(0, b, b1 : bool, x1, high1, b2 : bool, x2, high2) :FN_DB(x1, high1, x2, high2, b), b1, b2, x1 = x2.
Inv(d’, b, b1’ : bool, x1’, high1, b2 : bool, x2, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1 and (b1’ and x1’ = x1 + 1 or !b1’ and x1’ = x1) or!b1 and !b1’ and x1’ = x1,(!b1 or !b2 or d’ = d + 1).
Inv(d’, b, b1 : bool, x1, high1, b21 : bool, x21, high2),
Inv(d’, b, b1 : bool, x1, high1, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and !b22 and x22 = x1,(!b1 or !b2 or d’ = d - 1).
Inv(d, b, b1’ : bool, x1’, high1, b21 : bool, x21, high2),
Inv(d, b, b1’ : bool, x1’, high1, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1 and (b1’ and x1’ = x1 + 1 or !b1’ and x1’ = x1) or!b1 and !b1’ and x1’ = x1,
b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and !b22 and x22 = x1.
b1 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b2.

40

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
b2 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1.
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), b1 or b2.
-b <= d and d <= b and b >= 0 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), b1, b2.
high1 + x1 = high2 + x2 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), !b1, !b2.
WF_R2(b2 : bool, x2, high2, b21 : bool, x21, high2),
WF_R2(b2 : bool, x2, high2, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),!b1, b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2.

– The TS-GNI verification problem SimpleTS_GNI2 of the following program:x = high; while ( * ) { x ++; }; return x;

The encoded constraints are:Inv(0, b, b1 : bool, x1, high1, b2 : bool, x2, high2) :FN_DB(x1, high1, x2, high2, b), b1, b2, x1 = high1, x2 = high2.
Inv(d’, b, b1’ : bool, x1’, high1, b2 : bool, x2, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1 and (b1’ and x1’ = x1 + 1 or !b1’ and x1’ = x1) or!b1 and !b1’ and x1’ = x1,(!b1 or !b2 or d’ = d + 1).
Inv(d’, b, b1 : bool, x1, high1, b21 : bool, x21, high2),
Inv(d’, b, b1 : bool, x1, high1, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and !b22 and x22 = x1,(!b1 or !b2 or d’ = d - 1).
Inv(d, b, b1’ : bool, x1’, high1, b21 : bool, x21, high2),
Inv(d, b, b1’ : bool, x1’, high1, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1 and (b1’ and x1’ = x1 + 1 or !b1’ and x1’ = x1) orConstraint-based Relational Verification

41!b1 and !b1’ and x1’ = x1,
b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and !b22 and x22 = x1.
b1 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),b2.
b2 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
b1.
SchTF(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchFT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),
SchTT(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), b1 or b2.
-b <= d and d <= b and b >= 0 :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), b1, b2.
x1 = x2 :- Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2), !b1, !b2.
WF_R2(b2 : bool, x2, high2, b21 : bool, x21, high2),
WF_R2(b2 : bool, x2, high2, b22 : bool, x22, high2) :Inv(d, b, b1 : bool, x1, high1, b2 : bool, x2, high2),!b1, b2 and b21 and x21 = x2 + 1 and !b22 and x22 = x2.

– The TS-GNI verification problem InfBranchTS_GNI of the following program:if (high) {while (x>0) { x = x - max( * , 1); }} else {while (x>0) { x = x - 1; }}The encoded constraints are:Inv(0, b, high1 : bool, x1, high2 : bool, x2) :FN_DB(high1 : bool, x1, high2 : bool, x2, b), x1 = x2.
Inv(d’, b, high1 : bool, x1’, high2 : bool, x2) :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
SchTF(d, b, high1 : bool, x1, high2 : bool, x2),
high1 and x1 > 0 and FN_R(high1 : bool, x1, nd) and(nd >= 1 and x1’ = x1 - nd or x1’ = x1 - 1) and d’ = d + 1 or!high1 and x1 > 0 and x1’ = x1 - 1 orx1 <= 0 and x1’ = x1,

42Hiroshi Unno, Tachio Terauchi, and Eric Koskinen(x1 <= 0 or x2 <= 0 or d’ = d + 1).
Inv(d’, b, high1 : bool, x1, high2 : bool, x2’) :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
SchFT(d, b, high1 : bool, x1, high2 : bool, x2),
high2 and x2 > 0 and nd >= 1 and x2’ = x2 - nd or!high2 and x2 > 0 and x2’ = x2 - 1 orx2 <= 0 and x2’ = x2,(x1 <= 0 or x2 <= 0 or d’ = d - 1).
Inv(d, b, high1 : bool, x1’, high2 : bool, x2’) :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
SchTT(d, b, high1 : bool, x1, high2 : bool, x2),
high1 and x1 > 0 and FN_R(high1 : bool, x1, nd) and(nd >= 1 and x1’ = x1 - nd or x1’ = x1 - 1) or!high1 and x1 > 0 and x1’ = x1 - 1 orx1 <= 0 and x1’ = x1,
high2 and x2 > 0 and nd >= 1 and x2’ = x2 - nd or!high2 and x2 > 0 and x2’ = x2 - 1 orx2 <= 0 and x2’ = x2.
x1 > 0 :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
SchTF(d, b, high1 : bool, x1, high2 : bool, x2),
x2 > 0.
x2 > 0 :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
SchFT(d, b, high1 : bool, x1, high2 : bool, x2),
x1 > 0.
SchTF(d, b, high1 : bool, x1, high2 : bool, x2),
SchFT(d, b, high1 : bool, x1, high2 : bool, x2),
SchTT(d, b, high1 : bool, x1, high2 : bool, x2) :Inv(d, b, high1 : bool, x1, high2 : bool, x2), x1 > 0 or x2 > 0.
-b <= d and d <= b and b >= 0 :Inv(d, b, high1 : bool, x1, high2 : bool, x2), x1 > 0, x2 > 0.
top :- Inv(d, b, high1 : bool, x1, high2 : bool, x2), x1 <= 0, x2 <= 0.
WF_R1(high1 : bool, x1, high1 : bool, x1’) :Inv(d, b, high1 : bool, x1, high2 : bool, x2),
x2 <= 0,high1 and x1 > 0 and FN_R(high1 : bool, x1, nd) and(nd >= 1 and x1’ = x1 - nd or x1’ = x1 - 1) or!high1 and x1 > 0 and x1’ = x1 - 1.

– The TI-GNI verification problem TI_GNI_h** of the following program:if (high) {Constraint-based Relational Verification

43

x = *;
if (x >= low) { return x; } else { return low; }} else {x = low;while ( * ) { x++; }return x;}

The encoded constraints are:
Inv(pr (* prophecy variable for the return value of Copy 1 *),b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2) :b1, b2, low1 = low2,
high1 and x1 = nd1 or!high1 and x1 = low1,
high2 and FN_R(pr, high2 : bool, low2, x2) or!high2 and x2 = low2.
Inv(pr, b1’ : bool, x1’, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2) :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchTF(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
high1 and b1 and (x1 >= low1 and !b1’ and x1’ = x1 or
x1 < low1 and !b1’ and x1’ = low1) or!high1 and b1 and (b1’ and x1’ = x1 + 1 or
!b1’ and x1’ = x1) or!b1 and !b1’ and x1’ = x1.
Inv(pr, b1 : bool, x1, high1 : bool, low1, b21 : bool, x21, high2 : bool, low2),
Inv(pr, b1 : bool, x1, high1 : bool, low1, b22 : bool, x22, high2 : bool, low2) :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchFT(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
high2 and b2 and (x2 >= low2 and !b21 and x21 = x2 and!b22 and x22 = x2 or
x2 < low2 and !b21 and x21 = low2 and!b22 and x22 = low2) or!high2 and b2 and b21 and x21 = x2 + 1 and!b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and!b22 and x22 = x2.
Inv(pr, b1’ : bool, x1’, high1 : bool, low1, b21 : bool, x21, high2 : bool, low2),
Inv(pr, b1’ : bool, x1’, high1 : bool, low1, b22 : bool, x22, high2 : bool, low2) :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchTT(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
high1 and b1 and (x1 >= low1 and !b1’ and x1’ = x1 or
x1 < low1 and !b1’ and x1’ = low1) or!high1 and b1 and (b1’ and x1’ = x1 + 1 or
!b1’ and x1’ = x1) or!b1 and !b1’ and x1’ = x1,

44Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
high2 and b2 and (x2 >= low2 and !b21 and x21 = x2 and!b22 and x22 = x2 or
x2 < low2 and !b21 and x21 = low2 and!b22 and x22 = low2) or!high2 and b2 and b21 and x21 = x2 + 1 and!b22 and x22 = x2 or!b2 and !b21 and x21 = x2 and!b22 and x22 = x2.
b1 or pr <> x1 :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchTF(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),b2.
b2 :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchFT(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
b1 or pr <> x1.
SchTF(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchFT(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
SchTT(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2) :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),
b1 or pr <> x1 or b2.
x1 = x2 :Inv(pr, b1 : bool, x1, high1 : bool, low1, b2 : bool, x2, high2 : bool, low2),!b1 and pr = x1 (* if the prophecy is correct *), !b2.

In the experiment of TI_GNI_hFT, we provided the following constraint as ahint:x1 >= low1 :- Inv(pr, b1 : bool, x1, low1, b2 : bool, x2, low2).

Note that this is a part of necessary non-relational invariant.