Proofs as Relational Invariants of Synthesized Execution Grammars
CALEB VOSS, Georgia Institute of Technology
DAVID HEATH, Georgia Institute of Technology
WILLIAM HARRIS, Georgia Institute of Technology

arXiv:1710.03357v1 [] 10 Oct 2017

The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers
and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restricted forms, or
require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness.
In this work, we introduce a novel automatic safety verifier of programs that maintain low-level data structures, named Lttp. Lttp
synthesizes proofs of program safety represented as a grammar of a given program’s control paths, annotated with invariants that
relate program state at distinct points within its path of execution. Lttp synthesizes such proofs completely automatically, using a
novel inductive-synthesis algorithm.
We have implemented Lttp as a verifier for JVM bytecode and applied it to verify the safety of a collection of verification
benchmarks. Our results demonstrate that Lttp can be applied to automatically verify the safety of programs that are beyond the
scope of previously-developed verifiers.

1

INTRODUCTION

Automatically verifying that a given program satisfies a desired safety property is a fundamental problems of program
verification. Recent work has seen the development of powerful program verifiers that operate automatically [9, 22–
25, 38]. Such verifiers can often determine if practical programs satisfy properties concerning their control flow and
facts over a bounded collection of data values [5].
However, verifying the safety of programs that maintain unbounded low-level data structures remains an open
problem. A significant body of previous work has developed shape analyzers [17, 26] that, given a program P, synthesize
invariants of the reachable heaps of P represented in a particular shape domain, such as three-valued logical structures [35,
41, 45] or separation-logic formulas [12, 15, 42, 53]; the invariants synthesized by such analyzers can potentially imply
facts about program states that establish that P is safe. Another body of work has developed automatic program
verifiers [1, 4, 10, 14, 16, 19, 28, 29, 31, 34, 40, 43] and decision procedures [39, 46] that directly attempt to determine if
P is safe by attempting to synthesize sufficient invariants in such domains.
Unfortunately, all such approaches suffer from at least one of several critical limitations. In particular, they either
are only able to represent invariants over heaps of restricted forms [4, 14, 16, 28, 29, 31, 34] or require an analyst to
manually provide abstractions [1, 12, 14, 15, 17, 19, 26, 31, 39–43, 45, 46, 53] or candidate inductive invariants [10, 28].
The main contribution of this work is an automatic verifier, named Lttp, that attempts to determine the safety of a
program that may maintain low-level data structures. Lttp satisfies two key features that distinguish it from previous
approaches. First, it can potentially prove the safety of programs by establishing inductive invariants that relate multiple
low-level structures maintained by a program, each of which need not necessarily have a pre-specified shape, such as
© 2017 Copyright held by the owner/author(s). Manuscript submitted to ACM

1

list or tree. Second, Lttp performs synthesis of these invariants completely automatically, without requiring an analyst
to provide predicates over values or data-structure shapes from which to attempt to synthesize a proof.
We designed Lttp to satisfy both of the above features by developing two key technical insights. The first insight is
that the safety of a program that maintains low-level data structures can often be established by invariants that relate
only values bound to variables (i.e., local data) at multiple control points. Each proof structure synthesized by Lttp is an
annotated path grammar of the program—i.e., a graph grammar in which the yield of each derivation is a program
path. Each non-terminal A of the grammar is annotated with a formula that relates only the local values of a tuple of
program points generated by each application of A. Such a formula is in the combination of a theory that axiomatizes
the program’s data operations with the theory of uninterpreted functions.
The second insight is that proofs as relational invariants of graph grammars can potentially be synthesized automatically, using an inductive synthesizer [2, 47–50]. The inductive synthesizer implemented by Lttp, given a program
P, iteratively maintains a set of enumerated control paths of P. In each iteration, Lttp synthesizes a candidate graph
grammar G from the structure of P and enumerated paths by reduction to constraint solving. Lttp attempts to synthesize
relational invariants of G by reduction to logic programming [9, 44]. If a logic-programming solver determines that no
such invariants exist, then Lttp collects from the solver an unexplored control path which it uses to refine the proposed
grammar in subsequent iterations.
We have developed an implementation of Lttp that verifies programs represented in Java Virtual Machine (JVM)
bytecode. We evaluated Lttp by using it to attempt to verify the safety of a collection of challenging problems for shape
analyses and verifiers, some of which are adapted from those presented in the SV-COMP verifier competition [20].
The results demonstrate that Lttp is powerful enough to express non-local invariants, combining information
separated in time by unboundedly many execution steps and separated in heap space by unboundedly many field
accesses. Without manual assistance, Lttp can prove unary and binary properties over lists, reachability properties,
and even correlative properties between two disjoint data structures.
In summary, the design of Lttp builds on and contributes to multiple topics in program analysis and verification.
First, Lttp constitutes a shape verifier with strengths that are distinct from all shape verifiers presented in previous work,
though it does not necessarily subsume such verifiers, as discussed in §5.4. Second, Lttp demonstrates that techniques
from relational verification [6–8] which previously have been applied to prove properties of multiple programs by
relating states across multiple runs, can be applied to prove shape properties by relating states within program runs.
Third, Lttp demonstrates that techniques from inductive synthesis, which have previously been applied to synthesize
correct programs as completions of incomplete programs, can also be used to synthesize alternate representations of
complete programs that are amenable to verification.
The rest of this paper is organized as follows. §2 illustrates the operation of Lttp by example. §3 reviews previous
work on which Lttp is based, §4 describes the proofs synthesized by Lttp, and §5 describes Lttp’s inductive-synthesis
algorithm. §6 describes our empirical evaluation of Lttp. §7 compares Lttp to related work, and §8 concludes.
2

OVERVIEW

This section illustrates Lttp by example. §2.1 introduces an example program as a verification problem. §2.2 introduces
the proof of buildInspect synthesized by Lttp. §2.3 describes how Lttp synthesizes the proof automatically.
2.1 buildInspect: maintaining a low-level queue
2

1
2
3
4
5
6
7
8
9
10
11
12

class Element { Element next; }
public static void buildInspect(int num) {
Element head = new Element();
Element tail = head;
for (int i = 0; i < num; i++) {
Element tmp = new Element();
tail.next = tmp;
tail = tmp; }
Element elt = head;
for (int i = 0; i < num; i++)
elt = elt.next;
assert elt == tail; }

Fig. 1. buildInspect: constructs a queue with num elements and traverses it from head to tail.

a:
3
b:
5
i:
10

c:
7

d:
8
j:
11

e:
5
k:
10

f:
7

g:
8
l:
11

h:
5
m:
10
n:
12

Fig. 2. A control path of buildInspect containing two iterations of the loops, including data-dependence edges.

Figure 1 contains a program, named buildInspect, that maintains a low-level queue. The queue is represented as a
linked list of Element objects (line 1). buildInspect first constructs a single Element object and binds it to variables
that store both the queue’s head (line 3) and tail (line 4). buildInspect then iteratively creates new Elements and
adds them to the end of the queue (lines 5—8). buildInspect then iterates over the elements in the queue, storing
each element in elt (lines 10—11). Finally, buildInspect asserts that, on completion of the loop in lines 10—11, elt
stores the tail element of the queue (line 12).
Each execution of buildInspect satisfies the assertion at line 12. The key invariant for the loop over lines 5—8
establishes that the Element object stored in elt reaches the object stored in tail over some number i of dereferences
of the next pointer. The key invariant for the loop over lines 10—11 establishes that the Element object stored in elt
reaches the Element object stored in tail over num − i dereferences of the next pointer, where n is the length of the
queue. Unfortunately, it is challenging to design a verifier that can express such invariants and infer them automatically
from a given program without supplied candidate invariants.
2.2

A proof of buildInspect’s safety as relational invariants of a path grammar

A key insight behind our approach is that proofs of the safety of a program P can be represented as a graph grammar
that generates control paths of P, annotated with invariants that relate states at different path points when they co-occur
in the same grammar rule. In this section, we give a grammar GBI of buildInspect’s control paths (§2.2.1) and
relational invariants of GBI that represent a proof of the safety of buildInspect (§2.2.2).
2.2.1 A grammar of buildInspect’s control paths. Figure 2 contains the control path of buildInspect that
includes two iterations of the loop at lines 5—8 and two iterations of the loop at lines 10—11. In Figure 2, each node is
an instance of a control location, annotated with its line number. The line number of each node indicates the program
has reached, but not executed, the instruction on that line. Control steps are depicted as solid edges. Each point that
stores an object is connected to the point that loads the stored object by a dashed line.
A graph grammar GBI that generates the control paths of buildInspect is depicted in Figure 3. GBI contains two
relations, buildInspect and StLd, with buildInspect the starting relation. GBI consists of three clauses, one for
buildInspect and two for StLd. Each clause is depicted as a hypergraph. The nodes represent program control points
and are labeled with an alphabetic character for reference and with the corresponding line number in the program. The
edges consist of control-dependence edges, depicted as solid edges; the dashed edges depict data dependencies, and are
3

StLd[0]

buildInspect[0]
a:3

b:5

0

1

StLd
d:
10

2

3

StLd[1]

c:9

a:5

b:9

a:5

1
3

0

0

0
2

e:
12

c:
10

d:
12

b:7

c:8

d:5

StLd

2
f:
10

0 1

g:
11

h:
10

2 3

e:9

1
3
i:
12

Fig. 3. A graph grammar that generates buildInspect’s control paths and has relational invariants that prove the safety of
buildInspect. The grammar contains three clauses, each labeled with their head relation (either buildInspect or StLd).

described in §2.2.2. Each (ordered) hyperedge h is represented as a box labeled with a relation, and with the nodes in h
labeled with their index in h. The hyperedge that each clause defines is represented implicitly, with the nodes in the
hyperedge dashed and labeled with their index in the hyperedge.
The starting relation of GBI , buildInspect, has a single clause, buildInspect[0], that generates fragments of a
control path that model the initial step of buildInspect and the step of buildInspect from the exit of the loop at
lines 5—9 to the entry of the loop at lines 10—11.
The relation StLd simultaneously derives a pair of paths, corresponding to the two loops of the program. GBI
contains two clauses for StLd. Clause StLd[0] generates a pair of loop exit steps. Clause StLd[1] generates both a step
through the loop at lines 5—9 that allocates a new Element object and stores it at the next field of a bound object, and
a step through the loop at lines 10—11 that loads an Element object. Clause StLd[1] recursively includes an instance
of the StLd relation, which can be further expanded in order to generate the rest of each loop.
The control path in Figure 2 is generated by GBI . In particular, it is generated by applying the following sequences
of rules: buildInspect[0], StLd[1], StLd[1], StLd[0].
It should be noted that the grammar shown in Figure 3 is a simplification of the grammar required to prove the
safety of buildInspect. In particular, the depicted grammar only allows expansions of StLd such that the two loops
iterate the same number of times. It is true that every actual execution has this property, but this fact is not known a
priori. Therefore, the grammar must allow paths with different numbers of iterations in each loop so that the underlying
model checker can discover such an invariant through counterexamples.
2.2.2 Relational invariants of buildInspect’s path grammar. A second key observation that motivates our approach
is that a proof of the safety of a program P can be represented as some grammar G of the paths of P paired with
relational invariants over the location instances in the interface of each of the relations of G. In particular, a proof
of the safety of buildInspect can be represented as the path grammar GBI (given in §2.2.1), paired with relational
invariants over instances of control locations in the interface of buildInspect and StLd that establish that at the 0th
interface node of buildInspect, elt = tail.
The relational invariant for StLd establishes that if tail at index 0 is equal to elt at index 2 and if the point in the
path at which the next field of tail at index 1 was stored is the point at which the next field of elt at index 2 was
stored, then tail at index 1 is elt at index 3. It also establishes that i at index 0 is equivalent to i at index 2, indicating
4

Loop0[0,1]
3

Loop0

Loop1[0,1]
4

5

0
6

7

8

5

Loop0
Loop1

buildInspect[0]

0
5

9

10

Loop1

0
10

11

0
10

12

10

′ that generates ccbuildInspect’s control paths, but does not have relational invariants that
Fig. 4. An alternative graph grammar G BI
prove the safety of buildInspect.

that the loops will iterate the same number of times. The relational invariant for StLd can be expressed as the following
formula, where integer subscripts indicate interface node indices and next indicates a function which maps each object
to the path point at which it was last updated:
(tail0 = elt2 ∧ next1 (tail0 ) = next2 (elt2 ) =⇒ tail1 = elt3 ) ∧ i0 = i2

(1)

Formula 1 entails that each run of buildInspect satisfies its assertion at line 12. Furthermore, it can be proved to
hold over all tuples of path points in all paths generated by GBI , by induction on the derivations of GBI . In particular,
(1) in clause StLd[0], the semantic constraints of the instructions on generated control steps entail Formula 1 with the
variables at index 0, 1, 2, and 3 replaced with variables that represent state at points a, b, c, and d respectively. (2) In
clause StLd[1], semantic constraints of the instructions on generated control steps, combined with Formula 1 with the
variables at index 0, 1, 2, and 3 replaced with variables that model state at points d, e, h, and i, entail Formula 1 with
variables at index 0, 1, 2, and 3 replaced with variables that represent state at path points a, e, f , and i.
2.3

Proving safety of buildInspect automatically

Lttp, given a program P with an error location L, attempts to prove that L is unreachabale in P by synthesizing a path
grammar that has relational invariants that prove that L is unreachable in P. To prove that buildInspect always
satisfies the assertion at line 12, Lttp synthesizes the path grammar of buildInspect given in §2.2.1 and the relational
invariants of the grammar given in §2.2.2.
Lttp, given program P and error location L, attempts to synthesize a proof that L is unreachable in P as relational
invariants by performing an inductive synthesis algorithm [2, 21, 32, 51]. The algorithm maintains an initially empty
set of enumerated control paths of P.
In each iteration, Lttp synthesizes a graph grammar G that derives all control paths of P and that admits relational
invariants proving the safety of all paths enumerated. As the set of enumerated paths is initially empty, the first grpah
grammar synthesized by Lttp is likely a simple grammar whose structure directly corresponds to the control-flow
′ given in Figure 3, in which each path is derived left-recursively.
graph of buildInspect, such as the grammar G BI

′ given in Figure 3, in which each relation derives a single path leftE.g., it could synthesize the graph grammar G BI

recursively. As a heuristic, Lttp could initially synthesize path grammars that use right-recursive definitions, the
program’s syntactic structure, or other sub-structures of the program’s control-flow graph, such as components of its
Bourdoncle decomposition [11]. However, no such fixed grammar can serve as a proof of correctness in general, and
must be iteratively restructured.
5

After Lttp synthesizes a graph grammar G, it attempts to determine if G has relational invariants that represent a
proof of the safety of P. Lttp reduces this problem to solving a system S of Constrained Horn Clauses (see §3.2.2), and
runs a solver on the generated system as a black box. If the solver determines that S has a solution, then the solution
contains relational invariants of G that prove safety of P.
Otherwise, if the solver provides a counter-derivation D of S that has no solution, then D defines a control path
′ , Lttp determines that some
that cannot be proved safe by relational invariants of G. For example, when given G BI

′ , such as the one corresponding to the control path p given in Figure 2, has no solution. Such a
derivation of G BI
derivation has no solution because nodes of the path that are the sites of matching stores and loads do not co-occur in
′ .
the clauses of G BI

Lttp then inspects the control path of the unsolvable derivation and determines if it is truly unsafe. If so, then Lttp

determines that P is unsafe. Otherwise, as in the case of p, Lttp determines that the path is safe, adds it to the set of
′ that
enumerated paths, and recurses. In Lttp’s next iteration, it will synthesize a path grammar distinct from G BI

admits relation invariants proving the safety of p. Lttp eventually synthesizes G BI , which proves safety for all paths.

3

BACKGROUND

In this section, we review foundations on which Lttp is built. In §3.1, we define the low-level imperative language
targeted by Lttp. In §3.2, we review concepts from formal logic and logic programming used in the design of Lttp.

3.1

A target imperative language

In this section, we define the structure (§3.1.1) and semantics (§3.1.2) of Lttp’s target language.
3.1.1 Structure. A program is a set of instructions, each labeled with a control location and a target control location.
The space of all control locations is denoted Locs, with distinguished initial location and final location LI , LF ∈ Locs.
The finite spaces of value variables and object variables are denoted DVars and OVars, respectively; their union is
denoted Vars = DVars ∪ OVars. The finite spaces of data fields and object fields are denoted DFields and OFields,
respectively. All spaces of mutually disjoint. Lttp can be applied to programs in languages with infinite spaces of
variables and fields, because it only must consider the finite sets of variables and fields that occur in a given program.
We assume that the spaces of variables and fields themselves are finite in order to simplify the presentation of Lttp.
The space of data instructions is denoted InstrsV , and includes standard operations of Boolean and linear integer
arithmetic. Let p, q ∈ OVars, x ∈ DVars, f ∈ DFields, and g ∈ OFields be arbitrary elements. y:=p->f is a data load
and p->f:=y is a data store; q:=p->g is an object load and p->g:=q is an object store. The spaces of all data loads, data
stores, object loads, and object stores are denoted FieldsD , StoresD , LdsO , and StoresO , respectively. p:=new() is
an allocation, x:=isNil(p) is a nil test, and 1:=p=q is an object-equality test; the space of all allocations, nil tests, and
object-equality tests are denoted Allocs, NilTests, and ObjEqs, respectively. The space of all instructions is denoted
Instrs = InstrsV ∪ FieldsD ∪ StoresD ∪ LdsO ∪ StoresO ∪ Allocs ∪ NilTests ∪ ObjEqs
A pre-location, instruction, and branch-target location is a labeled instruction; i.e., the space of labeled instructions
is denoted LblInstrs = Locs × Instrs × Locs. For each labeled instruction i ∈ LblInstrs, the pre-location,
instruction, and post-location of i are denoted PreLoc[i], Instr[i], and BrTgt[i], respectively.
6

Instruction
i ∈ InstrsV
x:=p->f
p->f:=x
q:=p->f
p->f:=q
x:=p=q
x:=isNil(p)
p:=new()

Updated
Components

Updated Value

σD
σD
HD
σO
HO
σD
σD
σO
HD
HO

σ D′ ∈ CtxsV , σ D →V σ D′
i
σD [
x 7→H (σO (p), f)
]
HD [
(σO (p), f) 7→σ D (x)
]
q 7→H D (σ D (p), f)
]
σO [
HO [
(σO (p), f) 7→σO (q)
]
σD [
x 7→σO (p) = σO (q)
]
σD [
x 7→σO (p) = nil
]
σO [
p 7→o < Dom(HO ) = Dom(H D )]
H D [{o} × DFields 7→0
]
HO [{o} × OFields 7→nil
]

Table 1. Resulting post-state of instructions from, for σ D ∈ CtxsV , σO ∈ CtxsO , H D ∈ HeapsD , and HO ∈ HeapsO , the pre-state
((σ D , σO ), (H D , HO )). In each instruction, p, q ∈ OVars, x ∈ DVars, d ∈ DFields, and f ∈ OFields. In the entry for p:=new(),
for each map m, Dom(m) denotes the domain of m.

A program is a set of labeled instructions. I.e., the space of programs is Lang = P(LblInstrs), where for any set
S, P(S) denotes the powerset of S. For each P ∈ Lang and all L, L ′ ∈ Locs, there may be at most one i ∈ LblInstrs
such that PreLoc[i] = L and BrTgt[i] = L ′ . In such a case, i is denoted alternatively as Instr[P](L, L ′ ).
3.1.2 Semantics. A run of a program P is a sequence of states generated by a sequence of labeled instructions in
which adjacent instructions have matching target locations and pre-locations. The space of data is Data = B ∪ Z, the
space of non-nullable objects is a countably-infinite space Objs ′ , and the space of objects is Objs = Objs ′ ∪ {nil}.
The space of local data states is CtxsV = DVars → Data, the space of local object states is CtxsO = OVars → Objs,
and the space of local states is Ctxs = CtxsV × CtxsO . The space of data heaps is HeapsD = Objs ′ × DFields → Data,
the space of object heaps is HeapsO = Objs ′ × OFields → Objs, and the space of heaps is Heaps = HeapsD × HeapsO .
The space of states is States = Ctxs × Heaps.
For each i ∈ InstrsV , there is a transition relation →V ⊆ CtxsV × CtxsV . The transition relation of a value
i
instruction need not be total: thus, labeled instructions can implement control branches using instructions that act as
assume instructions. The transition relation of instructions is defined based on their structure. The transition relation
of each instruction, defined over an arbitrary pre-state, is given in Table 1.
For each labeled instruction i ∈ LblInstrs, the transition relation of i is the transition relation of the instruction
of i; i.e., →i =→Instr[i] . A program state σ may not be the source of any entry in the transition relation if it binds an
object variable p to nil and executes an instruction that attempts to load from or store to nil. For the remainder of this
paper, we do not consider a stuck state to be an error state; programs can be transformed so that stuck states are error
states in our formulation.
For each finite space N , E ⊆ N × N such that (N , E) is a sequential graph and each λ : N → Locs, (N , E, λ) is
a control path. For each P ∈ Lang, if (N , E, λ) is such that for all path edges (n, n ′ ) ∈ E, there exists an instruction
Instr[P](λ(n), λ(n ′ )), then (N , E, λ) is a control path of P. The space of control paths of P is denoted Paths[P]. For each
p ∈ Paths[P], the nodes of p are denoted Nodes[p].
A run of a program P is a control path p of P and a map from each node of p to a state such that states associated
with adjacent nodes satisfy the transition relation of a corresponding instruction of P.
7

Definition 1. For P ∈ Lang, finite space N , E ⊆ N × N , and λ : N → Locs such that (N , E, λ) ∈ Paths[P], let
σ : N → States be such that for all n, n ′ ∈ N with (n, n ′ ) ∈ E, σ (n) →Instr[P](λ(n), λ(n ′ )) σ (n ′ ). Then for p = (N , E, λ),
(p, σ ) is a run of p in P.
For p ∈ Paths[P], the runs of p in P are denoted Runs[p]. For r ∈ Runs[p], p is denoted alternatively as DerPathr .
If Runs[p] is empty, then p is infeasible. The runs of P are the runs of all paths of P; i.e., the runs of P are denoted
Ð
Runs[P] = p ∈Paths[P] Runs[p]. If Runs[P] is empty, then P is safe. The core problem addressed in this work is, given
program P, to determine if P is safe.
3.2

Constraint solving and Constrained Horn Clauses

3.2.1 Formal logic. The quantifier-free fragment of the theory of the combinations of linear arithmetic and uninterpreted functions is denoted EufLia. For each space of logical variables X , the space of EufLia formulas over X is
denoted Forms[X ]. For each formula φ ∈ Forms[X ], the set of variables that occur in φ (i.e., the vocabulary of φ) is
denoted V (φ). For formulas φ 0 , . . . , φ n , φ ∈ Forms[X ], the fact that φ 0 , . . . , φ n entail φ is denoted φ 0 , . . . , φ n |= φ. The
models of variables X are denoted Models[X ]. The fact that a model m satisfies a formula φ is denoted m ⊢ φ. Lttp uses
a decision procedure for EufLia, named IsSat. We assume that for each i ∈ InstrsV , Lttp may access some formula
SymRelV [i] ∈ Forms[EufLia].
3.2.2 Constrained Horn Clauses. Constrained Horn Clauses are a class of logic-programming problems that formulate
problems in program verification [9, 18, 22, 44].
Structure. A Constrained Horn Clause is a body, consisting of uninterpreted relational predicates applied to logical
variables and a constraint, and a head application. Relational predicates are symbols associated with arities.
Definition 2. For each space of symbols R and function a : R → N, (R, a) is a space of relational predicates.
An application is a relational-predicate symbol paired with a sequence of logical variables of length matching its
arity. To simplify the presentation, all objects defined in the remainder of the section are defined over a fixed space of
predicate symbols R in which each symbol has arity k ∈ N, and a fixed space of logical variables X .
Definition 3. For relational predicate R ∈ R and sequence of variables Y ∈ X ∗ such that |Y | = k, (R, Y ) is an
application of R over X .
The space of applications of symbols in R over X is denoted Apps[R, X ]. For each application A ∈ Apps[R, X ],
the predicate symbol and argument sequence of A are denoted Rel[A] and Args[A] respectively. A clause is a set of
applications, a constraint over logical variables, and a head relational predicate.
Definition 4. For B ∈ Apps[R, X ]∗ , φ ∈ Forms[X ], and H ∈ R, (B, φ, H ) is a Constrained Horn Clause.
The space of Constrained Horn Clauses over R and X is denoted CHC R,X . For each C ∈ CHC R,X , the body of
applications, constraint, and head of C are denoted Apps[C], Ctr[C], and Head[C], respectively. A set of Constrained
Horn Clauses and a query relational-predicate symbol is a system of Constrained Horn Clauses; i.e., the space of systems
of Constrained Horn Clauses is denoted CHCs R,X = P(CHC R,X ) × R.
8

Models. A model of S is a collection of logical models that certify that S does not have a solution. A derivation
of a CHC system S is a tree D labeled with relational predicates of S such that all children with a common parent
p are labeled with relational symbols of applications in the body of a common clause of S with p as its head. For
C ⊆ CHC R,X , let each relational predicate that is not the head of any clause of C be a ground relational predicate of C.
Definition 5. For C ⊆ CHC R,X and Q ∈ R, E ⊆ N ∗ × N × C, and λ E : E → C be such that (N , E) is an directed
hypertree and there is some labeling function λ N : N → R such that: (1) for r ∈ N the root of (N , E), λ N (r ) = Q;
(2) for each n ∈ N a leaf of (N , E), λ N (n) is a ground relational predicate of C; (3) for all n 0 , . . . , nk , n ∈ N with
e = ([n 0 , . . . , nk ], n) ∈ E, it holds that (a) λ N (n) = Head[λ E (e)] and (b) for each 0 ≤ i ≤ k, λ N (ni ) = Rel[Apps[C]i ].
Then (N , E, λ E ) is a derivation of (C, Q).
For S ∈ CHCs R,X , the space of derivations of S is denoted Ders(S). For each D ∈ Ders(S), the nodes and hyperedges
of D are denoted Nodes[D] and HypEdges(D).
A model of a CHC system S is a derivation D of S and a model indexed on nodes of D that satisfies the clauses that
label the edges of D.
Definition 6. For S ∈ CHCs R,X , finite space N , E ⊆ N ∗ × N , λ E : E → Clauses[S] such that (N , E, λ E ) ∈ Ders(S),
let m be an EufLia model and let i : N → Models[X ] be such that for all n, n 0 , . . . , nk ∈ N and each C ∈ Clauses[S] with
e = ([n 0 , . . . , nk ], n) ∈ E, it holds that for C = λ E (e), (1) m, i(n) ⊢ Ctr[C]; (2) for each 0 ≤ j ≤ k, i(m)(Args[Apps[C]j ]) =
i(n j )(Params). Then (D, m, i) is a model of S.
We denote the models of S as Models[S]. For each D ∈ Ders(S), if there is some EufLia model m and i : Nodes[D] →
Models[X ] such that (D, m, i) is a model of S, then D is feasible; otherwise, D is infeasible. If some derivation of S is
feasible, then S is feasible (otherwise, S is infeasible).
A CHC solver is a procedure that, given CHC system S, returns either the value Infeas to denote that S is infeasible,
or a model of S; several CHC solvers have been proposed in previous work [9, 44]. Lttp uses a CHC solver, named
SolveCHC, as a black box.
Solutions. A solution of a clause C is an interpretation of relational predicates such that the conjunction of interpretations of all relational predicates in the body of C and the constraint of C entail the interpretation of the head of C. A
solution of a CHC system S is a solution of each clause in S that interprets the query relational predicate of S as an
unsatisfiable formula.
Definition 7. For C ⊆ CHC R,X and Q ∈ R, let i : R → Forms[Params] be such that under each EufLia model, (1)
for each B ∈ Apps[R, X ]∗ , H ∈ R, and φ ∈ Forms[X ] such that (B, H, C) ∈ C,
{i(Rel[A])[Vars[A]]}A∈B , φ |= i(H )
(2) i(Q) |= False. Then i is a solution of (C, Q).
When a CHC solver determines that a given system is empty, the solver can synthesize a solution that certifies
emptiness. If Lttp runs SolveCHC on a system S and SolveCHC determines that S is empty, then Lttp does not
require SolveCHC to provide the generated solution. However, Lttp could be adapted to generate the CHC system that
it synthesizes, accompanied by its solution found by SolveCHC, as a proof of safety that can be independently certified.
9

4

PROOFS AS RUN GRAMMARS

In this section and §5, we present Lttp in technical detail. In this section, we give a class of proofs of program safety as
grammars of program runs annotated with invariants.
Lttp, given program P, attempts to determine whether or not P is safe by synthesizing a CHC system S such that (1)
each run of P corresponds to a model of S and (2) S has no models. Lttp attempts to certify that S has no models by
synthesizing a solution of S in the theory TD,Uif . Let P be a fixed, arbitrary program for the remainder of the section.
Let the theory TLang be TD,Uif restricted to contain the following uninterpreted function symbols. The nullary
symbols of TLang contain, for each L ∈ Locs, the symbol L. The unary symbols of TLang contain symbols Loc and
Succ; for each x ∈ DVars, the symbol x; for each p ∈ OVars, the symbol p. The binary symbols of TLang contain for
each f ∈ DFields, the symbol f; for each g ∈ OFields, the symbol g.
If for each m ∈ Models[S] with domain N , the graph (N , ≻m , Locm ) is a control path of P, then S is a run grammar
of P. The space of run grammars of P is denoted CHCsLang P. Let S ∈ CHCsLang P be a fixed, arbitrary element for
the remainder of the section.
Lttp uses a procedure DerPath that, given m ∈ Models[S], returns the control path of the run of m. DerPath is
implemented by returning the interpretations of symbols Loc and Succ in m.
Each run r defines a map for each data and object field f, from each control point p of r and object o allocated while
executing r to the control point in r at which the f field of o was last updated when r reached p. In particular, let N be
a finite space, L : N → Locs; ≻: N → N ; σ : N → States be such that ((N , ≻, Loc), σ ) ∈ Runs[P]. For each x ∈ DVars,
xr : N → Vals is such that for each n ∈ N , xr (n) = σ (n)(x), and for each p ∈ OVars, pr : N → Objs is defined similarly.
For each f ∈ DFields, let cc fr : N × Objs → N be such that for all ni , n j ∈ N and o ∈ Objs, if ni is the last node
before n j such that Instr[P](Loc(ni−1 ), ni ) ≡ p->f:=x and σ (ni )O (x) = o, then fr (n j , o) = ni . For each g ∈ OFields,
let gr : N × Objs → N be defined similarly. Both collections of symbols are called update histories.
For S ∈ CHCsLang P, let domain N combined with L, ≻, {xr | x ∈ DVars}, {pr | p ∈ OVars}, {fr | f ∈ DFields},
{fr | f ∈ OFields} as interpretations of Loc, Succ, DVars, OVars, DFields, and OFields be the model of TLang
denoted mr . If mr is a model of S, then r is a run of S. If each run of P is a run of S, then P is simulated by S.
For p ∈ Paths[P], if for each r ∈ Runs[p], mr is not a model of S, then p is refuted by S. For Q ⊆ Paths[P], if for each
p ∈ Q, it holds that p is refuted by S, then Q are refuted by S. If Paths[P] are refuted by S, then P is refuted by S.
If a program is simulated and refuted by a CHC system, then the program is safe.
Lemma 1. If P is simulated by S and P is refuted by S, then P is safe (§3.1.2).
If P is simulated by a run grammar S, then a solution of S (which certifies that S is infeasible and thus refutes P),
can be viewed as relational invariants that prove the safety of P.
Example 1. Recall GBI , the grammar partially depicted in §2.2.1, Figure 3. If we encode the runs of buildInspect
using the structure of GBI , we could simulate every run, and showing the emptiness of that grammar could show the safety
of buildInspect.
However, a safe program P may be simulated by a CHC system that does not refute it.
′ , the simplistic grammar proposed in Figure 4. If we try to encode P using this structure, we are
Example 2. Recall GBI
compelled to overapproximate by dropping state information because an unbounded separation arises between a load and
10

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Input : P ∈ Lang.
Output : Decision as to whether P is safe.
Procedure Lttp(P)
Procedure Lttp ′ (F )
G := SynGrammar(P, F ) ;
switch SolveCHC(G) do
case Infeas: do
return True
case D ∈ Ders(G): do
p := DerPath(D) ;
if IsFeas(p) then
return False ;
else
return Lttp ′ (p ∪ {F }) ;
end
end
end
return Lttp ′ (∅)

Algorithm 1: Lttp: a safety verifier based on inductive synthesis. Lttp uses procedures SynGrammar
(§5.2, §5.3), SolveCHC (§3.2.2), DerPath (§4), and IsFeas
(§5.1.1).

1
2
3
4
5

6
7

Input : P ∈ Lang and p ∈ Paths[P].
Output : A minimal refuting neighborhood
ν : Nodes[p] → P(Nodes[p]) for p.
Procedure Deps(P, p)
ν := ν All ;
for n, n ′ ∈ Nodes[p] do
ν ′ := ν [n 7→ ν (n) \ {n ′ }] ;
if ¬IsSat(SymPath(P, p, ν ′ )) then ν := ν ′
;
end
return ν

Algorithm 2: Deps: given P ∈ Lang and infeasible
p ∈ Paths[P], returns a minimal refuting neighborhood for p. The map ν All and the formula SymPath
are defined in §5.1.1.

′ , but there are additional models not corresponding to
its matching store. Every runs of buildInspect is present in GBI

actual runs. This non-empty grammar simulates buildInspect, even though buildInspect is safe.
5

INDUCTIVE SYNTHESIS OF PROOFS USING LTTP

In this section, we describe Lttp, a verifier that attempts to prove the safety of a given program by inductively
synthesizing a run grammar as proof.
Alg. 1 contains pseudocode for Lttp. Lttp defines a procedure Lttp’ which, given infeasible paths F ⊆ Paths[P],
attempts to determine if P is safe by synthesizing a run grammar that overapproximates the runs of P and refutes F
(line 2—line 15). Lttp invokes Lttp’ on the empty set of control paths and returns the result (line 16).
Lttp’, given F , synthesizes a run grammar G that simulates P and refutes F by a procedure SynGrammar on P and
F (line 3). An implementation of SynGrammar that performs a reduction to constraint solving is described in §5.3.
Lttp’ then determines if G refutes P by running the CHC solver SolveCHC (described in §3.2.2) on G to determine if
G is infeasible. If SolveCHC determines that G is infeasible (line 5), then Lttp’ returns that P is safe.
Otherwise, SolveCHC returns a feasible derivation D of G (line 7). Lttp’ extracts from D some p ∈ Paths[P] not
refuted by G (line 8). Lttp’ then tests if p is feasible by running a procedure IsFeas on p (line 9); if IsFeas determines
that p is feasible, then Lttp’ returns that P is not safe.
Otherwise, if IsFeas returns that p is feasible, then Lttp’ recurses on F extended with p, and returns the result of the
recursion (line 12).
We now describe the implementation of each procedure used by Lttp. In §5.1, we describe an implementation of
IsFeas. In §5.2 and §5.3, we describe the two steps performed by SynGrammar.
11

5.1

Testing path feasibility using IsFeas

The procedure IsFeas, given P ∈ Lang and p ∈ Paths[P], returns whether or not p is a feasible path of P. Let finite
space N , E ⊆ N × N , and λ : N → Locs, be such that p = (N , E, λ). IsFeas generates a constraint φ ∈ Forms[TLang ]
for which each model corresponds to run of p.
5.1.1 Symbolic constraints over update histories. φ is constructed as a conjunction of clauses, each of which models
the effect of an instruction executed in a step of p on its local variables and update histories. The effect of each i ∈ P
executed in a step of p is formulated by a constraint SymRel[i] parameterized on N , along with distinguished n, n ′ ∈ N
that model state before executing i and state that immediately results from executing i.
SymRel[i](n, n ′, N ) is defined casewise by the structure of i. In many cases, SymRel[i] is defined using formulas that constrain equality of logical terms that model state. In particular, let EqDVars[n, n ′ ], EqOVars[n, n ′ ],
EqDFields[n, n ′, N ], and EqOFields[n, n ′, N ] constrain that the states at q and n ′ have equal local value states, local
object states, data timestamps, and object timestamps, respectively. I.e.,
Û
EqDVars[n, n ′ ] ≡
x(n) = x(n ′ )
x ∈DVars
Û
′
EqDFields[n, n , N ] ≡
f(n, p(n ′′ )) = f(n ′, p(n ′′ ))
f ∈DFields
p ∈OVars
n ′′ ∈N

EqOVars[n, n ′ ]

and

EqOFields[n, n ′, N ]

are defined similarly.

If i ∈ InstrsV , then SymRel[i] constrains that the value local state at n and the value local state at n ′ are in the
transition relation of i, and that their object stores are identical. I.e., SymRel[i](n, n ′, N ) is
SymRelV [i][DVars(n), DVars(n ′ )] ∧ EqOVars[n, n ′ ]∧
EqDFields[n, n ′, N ] ∧ EqOFields[n, n ′, N ]
For each i ∈ NilTests or i ∈ ObjEqs, the constraint SymRel[i] is defined similarly.
For x ∈ VarsV , p ∈ OVars, and f ∈ DFields, SymRel[p->f:=x](n, n ′, N ) constrains that at n ′ , the most recent
store to the f field of the object bound to p is n ′ . The local states and update history of all other fields are identical
between n and n ′ . I.e., SymRel[p->f:=x](n, n ′, N ) is
Û

EqDVars[n, n ′ ] ∧ EqOVars[n, n ′ ] ∧ f(n ′, p(n ′ )) = n ′ ∧

f(n ′, p(n ′′ )) = f(n, p(n ′′ ))∧

p ∈OVars
Û

′

′′

′′

n ′′ ∈N
′

g(n , p(n )) = g(n, p(n )) ∧ EqOFields[n, n , N ]

g,f ∈DFields
p ∈OVars
n ′′ ∈N

For each i ∈ StoresO , the constraint SymRel[i] is defined similarly.
Example 3. buildInspect contains an object store on line 7. The relation which models this instruction constrains
the local state after the instruction such that the most recent store for the next field of the object tail is set to tmp.
For each x ∈ DVars, p ∈ OVars and f ∈ DFields, SymRel[x:=p->f](n, n ′, N ) inspects all states bound to variables
in Q to determine if some n ′′ ∈ N is the point of the most recent store to f. If so, the value in x at n ′ is constrained to be
12

the value stored when stepping to n ′ ; otherwise, the value bound to x at n ′ is unconstrained. Let DStoreLocP ⊆ Locs be
control locations that are sources of data stores in P, and let Stored[P] : DStoreLocP → DVars map each such control
location to the data variable that holds that value stored by the instruction. Then SymRel[x:=p->f](n, n ′, N ) is
Û
f(q, p(q)) = n ′′ =⇒ x(q ′ ) = Stored[P](n ′′ )∧
n ′′ ∈N , λ(n ′′ )∈DStoreLocP

Û

y(n ′ ) = y(n) ∧ EqOVars[n, n ′ ] ∧ EqDFields[n, n ′, N ] ∧ EqOFields[n, n ′, N ]

y,x ∈DVars
For each i ∈ LdsO , the constraint SymRel[i] is defined similarly.
Example 4. buildInspect contains an object load on line 11. The relation which models this instruction constrains
the local state after the instruction such that the variable elt is set to the most recent store for the next field of the object
elt.
For x ∈ OVars, SymRel[x:=new()](n, n ′, N ) constrains that the identity of the allocated object is n ′ ; the fields of the
allocated object are initialized at n ′ .
EqDVars[n, n ′ ] ∧ x(n ′ ) = n ′ ∧

Û

y(n ′ ) = y(n) ∧ Stored(n ′ ) = 0∧

y,x ∈OVars
Û

′

f(n , x(n ′ )) = n ′ ∧

f ∈DFields∪OFields

Û

f(n ′, y(n ′ )) = f(n, y(n))

y,x ∈OVars
f ∈DFields∪OFields

For a path p = (N , λ, E) ∈ Paths[P], define the constraint SymPath(P, p, ν ) ∈ Forms[TLang ], where ν : N → P(N ),
as follows:
Û

SymRel[Instr[P](λ(n), λ(n ′ ))](n, n ′, ν (n ′ ))

(n,n ′ )∈E

Let ν All : N → P(N ) be such that for each n ∈ N , ν All (n) = N . IsFeas generates the constraint φ = SymPath(P, p, ν All ).
IsFeas returns that p is a feasible path of P if and only if IsSat (see §3.2.2) decides that φ is satisfiable.
IsFeas is a sound and complete procedure for testing path feasibility.
Lemma 2. If p is a feasible path of P, then IsFeas(P, p) = True. Otherwise, IsFeas(P, p) = False.
IsFeas could be implemented alternatively by reduction to satisfiability testing in alternative theories that can soundly
and completely model the feasibility of bounded paths, such as combinations of the theory of arrays. We have presented
IsFeas as using IsSat in order to introduce the symbolic relations on update histories for each instruction, which Lttp
also uses in queries in order to synthesize run grammar skeletons (§5.2), and as components of run grammars (§5.3).
5.2

Synthesizing a run-grammar skeleton using constraint solving

In this section and in §5.3, we describe an implementation of SynGrammar, which given P ∈ Lang and F ⊆ Paths[P],
synthesizes a run grammar G that simulates P and refutes F. SynGrammar synthesizes such a run grammar by
performing two steps, described in this section and §5.3. In the first step, SynGrammar finds the relations of G and the
sets of variables in each clause body to which relational predicates are applied. We refer to such an object as a CHC
system skeleton. SynGrammar finds a skeleton by reduction to constraint solving.
SynGrammar obtains a clause skeleton for P and F by running a procedure SynSkeleton on P and F. The implementation of SynSkeleton that we present always makes progress, in the sense that for each P and F, it synthesizes a
13

well-formed skeleton for P and F. However, the implementation is not complete, in that there are some safe programs
whose required skeletons are not expressible in this particular constraint-based approach to SynSkeleton. We have
found that the present implementation is sufficiently expressive for Lttp to be able to prove correctness of interesting
verification challenge problems (discussed in §6). We leave the design of alternative, more expressive, or more efficient
implementations of SynSkeleton for future work.
5.2.1 Run-grammar skeletons. In its first step, SynGrammar synthesizes a run-grammar skeleton, which defines the
control paths generated by run grammar constructed from completing it. We define a restricted implementation of
SynGrammar that only generates run grammars in which each non-terminal derives exactly two control subpaths of P.
In particular, let RSkel be a set of relational predicates of fixed, common arity n. Let Q be a space of variable symbols, and
let Q ′ ∈ Q ∗ be fixed sequence of n distinct variables in Q. For R ∈ RSkel , A ∈ Apps[RSkel , Q], L : Q → Locs, q, q ′ ∈ Q,
C = (R, A, L, q, q ′ ) is a clause skeleton. The space of clause skeletons is denoted ClauseSkels. A set of clause skeletons
combined with four maps from RSkel → Zn is a run-grammar skeleton. For the remainder of this section, let R, A, L, q,
q ′ , and S ⊆ ClauseSkels and F = Pre0 , Post0 , Pre1 , Post1 : RSkel → Zn be a fixed, arbitrary elements.
Synthesizing a skeleton that simulates a given program. (S, F ) simulate P if when each clause in S is extended
with a suitable constraint to form a clause, the resulting run grammar generates all control paths of P. In particular,
for φ ∈ Forms[TLang ], let ((A, φ), R) be the completion of C. Let S ′ ∈ CHCsLang such that each clause in S ′ is a
Ó
completion of a clause (R, A, L, q, q ′ ) with a constraint q ∈Q Loc(q) = L(q) ∧ q ′ = Succ(q) be the control-path grammar
of S. If for each R ′ ∈ RSkel and each model m of R, there is a control path from m(Pre0 (R ′ )) to m(Post0 (R ′ )) and a
control path from m(Pre1 (R ′ )) to m(Post1 (R ′ )), then (S, F ) is well-formed. If S ′ simulates p, then S simulates P. If all
r , r ′ ∈ Runs[S ′ ] that have the same control path have the same derivation in S ′ , then S is unambiguous.
SynSkeleton synthesizes a well-formed, unambiguous control-path grammar that simulates P by reduction to
constraint solving. In particular, Lttp generates an EufLia constraint φ P such that each model of φ P defines a set of
clause skeletons that simulate P. For each clause skeleton C, the problem of choosing a relational predicate to apply in
the body of C, the set of variables to which it is applied, the map from variables to locations, and instruction source and
destination variables can be encoded directly as an EufLia constraint.
Synthesizing a skeleton that refutes control paths. C refutes F if for each p ∈ F , the derivations of the control extension
of C simultaneously derive sufficient sets of matching loads and stores in p that a suitable extension of C (described in
§5.3) refutes p. Such sufficient sets are formulated precisely as a minimal refuting neighborhood of p.
For p ∈ F with N = Nodes[p] and ν : N → P(N ) such that SymPath[P, p, ν] is unsatisfiable, ν is a refuting
neighborhood of p. For all ν, ν ′ : N → P, if for all n ∈ N , ν ′ (n) ⊆ ν (n ′ ), then ν ′ is contained by ν ; if, in addition, ν is not
contained by ν ′ , then ν ′ is strictly contained by ν . If for each ν ′ : N → P(N ) that is strictly contained by ν , it holds
that ν ′ is not refuting neighborhood of p, then ν is a minimal refuting neighborhood of p.
Deps (Alg. 2), given P and an infeasible p ∈ Paths[P], returns a minimal refuting neighborhood of p. Deps maintains a
refuting neighborhood of p, from which it iteratively minimizes entries until it obtains a minimal refuting neighborhood.
Deps constructs ν All as an initial refuting neighborhood (line 2). For all n, n ′ ∈ N , it determines if the map ν ′ obtained
by removing n ′ from the image of n in its maintained refuting neighborhood ν (line 4) is a refuting neighborhood. To
determine this fact, Deps runs IsSat on SymPath[P, p, ν ′ ] (line 5). If ν ′ is a refuting neighborhood, then Deps updates
its maintained refuting neighborhood to be ν ′ (line 5).
14

For each p ∈ F with N = Nodes[p], SynSkeleton synthesizes a minimal refuting neighborhood of p, named
ν p : N → P(N ) by running Deps on P and p. SynSkeleton then constructs a constraint φ p in which each solution
defines (1) a set of clause skeletons, over the vocabulary interpreted as a clause skeleton in each solution of φ P , and (2)
a derivation D of p in which for each n ∈ N and each n ′ ∈ ν p (n), n and n ′ are derived in a common instance of a clause
in D.
′ , the simplistic grammar of Figure 4. As a skeleton, G ′ fails to refute even a short
Example 5. Recall once again GBI
BI

infeasible path of buildInspect. For example, if a path performs a store and a load (the transitions from line 7 to 8 and
from line 11 to 10), a refuting neighborhood must put the state at line 10 into the neighborhood of the state at line 8 or
′ to include a special case rule for this path. A better way is to construct the
vice versa. One way to do this is to modify GBI

grammar GBI from Figure 3, which refutes much large set of infeasible paths. In fact, this skeleton refutes all paths in
buildInspect.
We have described a particular implementation of SynSkeleton that we have implemented in the current version
of Lttp. The current of implementation of SynSkeleton is restricted, in that it only synthesizes skeletons of run
grammars that are linear and unambiguous. SynSkeleton finds such skeletons by reduction to constraint solving. The
key motivation for adopting such limitations was that a relatively simple but useful version of SynSkeleton could
be designed by reusing existing, heavily-optimized algorithms implemented in constraint solvers. However, Lttp
only requires that an implementation of SynSkeleton, given program P and infeasible paths F, synthesize a skeleton
encodes all paths of P, including refuting neighborhoods for the paths inF. Alternative, explicit implementations of
SynSkeleton may yield significant benefits over the current version based on constraint solving.
5.3

Synthesizing a run grammar from a skeleton

In its second step, SynGrammar completes C ⊆ Skels, a set of clause skeletons that simulates P and a refutes
F synthesized by SynSkeleton, to generate a run grammar G ∈ CHCsLang that simulates P and refutes F. Let
R ∈ RSkel , L : Q → Locs, q, q ∈ Q be such that (R, L, q, q ′ ) ∈ Skels. From (R, A, L, q, q ′ ), SynGrammar generates
φ ∈ Forms[TLang ], and includes in G the clause C = (A, φ, R).
φ is a conjunction of constraints that model the effect of i, and effects of allocations and stores performed in steps of
execution other than i (§5.3.1). The first conjunct φ 0 constrains that each instance of q ′ is a control success of each
instance of q; i.e., φ 0 ≡ q ′ = Succ(q). The second conjunct φ 1 constrains that for path points n and n ′ bound to q
and q ′ at an instance of C ′ , the state at n ′ is the result of transitioning from the state at n, under the instruction that
connections n and n ′ . I.e., φ 1 ≡ SymRel[Instr[P](L(n), L(n ′ ))](q, q ′, Q).
The third conjunct φ 2 models the effect of all instructions that connect points derived by other clause instances on
the objects in scope when the step of C executes. The construction of the constraint is described in detail below.
5.3.1 Formulating the effect of instructions derived outside of a clause instance. The space of valid runs with update
histories is partially constrained by the symbolic relations for each instruction, defined in §5.1.1. For each i ∈ Instrs,
SymRel[i] models the effect of executing i on a finite set of states. When SymRel[i] is used to determine feasibility of
an entire path, in which case the set consists of all states in the path. When SymRel[i] is used as a conjunct of a clause
constraint, the set of states consists of all states that are derived in the same instance of a clause C that derives the
states connected by i. However, it does not include the set of all states in the derived path, namely states that occur
15

exclusively in subderivations of C, or that occur in a subderivation outside of the derivation of C and are not provided
as arguments to C.
φ 3 constrains the effect of instructions executed in steps from such states on objects that may only be bound to
object variables in states derived in an application of C. If i is not an object load or allocation, then each object in scope
bound to a variable in an application of C is in scope for its child or and parent; as a result, φ ≡ True.
Otherwise, let p ∈ OVars be the object variable bound by i. Then φ 3 is a conjunction of two constraints. Let

R A ∈ RSkel and Q A ∈ Q ∗ be such that A = R A (Q A ). The first constraint, φ 30 ∈ Forms[TLang ], constrains that if the
object o bound to p at q is not in the scope of any states bound to Q A , then the update histories of o is identical across
both control subpaths derived by the derivation with head A. I.e., φ 30 is
Û
p(q) , p ′ (q ′′ ) =⇒
q ′′ ∈Q A

p′ ∈OVars
Û
f(Q A [Pre0 (R A )], p(q)) = f(Q A [Post0 (R A )], p(q))∧
f ∈OFields∪DFields
f(Q A [Pre1 (R A )], p(q)) = f(Q A [Post1 (R A )], p(q))
The second constraint, φ 31 ∈ Forms[TLang ], constrains that if o is not in an argument of R when C is applied, then the

update histories of o is identical between the end of the first control subpath that it derives and the beginning of the
second control subpath that it derives. I.e., φ 31 is
Û
p(q) , p ′ (q ′′ ) =⇒
q ′′ ∈Q ′

p′ ∈OVars
Û
f(Q ′ [Post0 (R)], p(q)) = f(Q ′ [Pre1 (R)], p(q))
f ∈OFields∪DFields
5.3.2 Key properties. The partial correctness of Lttp depends only on the fact that SynGrammar, given a program
and set of infeasible paths, synthesizes a run grammar that simulates the program.
Lemma 3. P is simulated by SynGrammar (P, F).
SynGrammar also synthesizes a run grammar that refutes F. However, this fact is primarily useful for proving that
Lttp’ progresses, in that it never collects the same control path from distinct invocations of SolveCHC.
5.4

Key features

Lttp is correct on all programs on which it terminates.
Theorem 1. If Lttp(P) = True, then P is safe, and if Lttp(P) = False, then P is not safe.
Because the problem of verifying safety of programs in Lang is undecidable, there are some programs on which
Lttp will not terminate.
One limitation of Lttp as presented above is that it can only effectively determine the safety of programs that contain
all stores of objects that they load. Defining a logic of program summaries that Lttp can both use and validate is a
conceptually challenging and critical direction for future work. Lttp is motivated by a number of practical applications
which it can be applied to. However, having a program summary logic would enable a direct and formal comparison on
the theoretical level to other approaches, particularly separation logic [42] and effectively propositional reasoning [29].
16

5.5

Discussion

The prototype of SynSkeleton, developed in §5.2, has some shortcomings which make it worthwhile to pursue a
replacement. It is deficient in the expressivity of the grammars it can return, and it is intractable on modest programs. For
an infeasible path p in the feedback set F , the existing constraint-based approach cannot enforce that every derivation of
p include a refuting neighborhood ν for p, merely that one such derivation does; hence, the expressivity of SynSkeleton
must be artificially limited to unambiguous grammars. If it were possible to additionally supply negative examples to
SynSkeleton (graphs of p not including any refuting neighborhood), then ambiguity would be permissible.
Learning a linear string grammar (a regular expression) through queries to an oracle is a solved problem due to
Angluin’s L∗ algorithm [3]. To be precise, one supposes a teaching oracle which can answer membership queries for
a secret language L and which can confirm or deny with a counterexample that a proposed DFA D has the property
L(D) = L. L∗ is an efficient algorithm for using this oracle to learn such a D through both positive and negative
examples. L∗ is guaranteed to terminate when L is regular. The parallel between this problem statement and the task of
SynSkeleton in Lttp is striking. In Lttp, a grammar C for an unknown language of graphs is sought. IsFeas(P, p, ν )
answers the query of whether the control path graph p = (N , λ, E) unioned with the data edges E Data implied by ν is a
member of this language. When a run grammar G is proposed, SolveCHC(SynGrammar(P, F )) attempts to confirm or
deny with a counterexample that G correctly describes the language.
The task of SynSkeleton is more difficult than the regular language learning task of L∗ because the unknown
language is a set of graphs, not strings. However, there is work towards L∗ -like algorithms for richer classes of
languages such as learners of context-free grammars [3, 13, 54] and multiple context-free (MCF) grammars [55]. A single
non-terminal symbol in an MCF grammar is not a hole in a single string, but a vector of r holes, where the rank r is
bounded. The rule for a non-terminal of rank r can invoke other non-terminals of rank r by producing characters at the
holes, of rank less than r by filling a hole, and of rank greater than r by splitting a hole into two adjacent holes. Again,
a striking parallel with Lttp arises: this behavior of MCF non-terminals is exactly the behavior of skeleton grammars
returned by SynSkeleton, where control edges play the role of characters. It remains an open question to determine if
an MCF learner can be adapted to include the data edges of a refuting neighborhood ν for each positive example p.

6

EVALUATION

We empirically evaluated Lttp in order to answer the following questions: (1) Can Lttp verify the safety of low-level
programs that operate on unbounded data structures where existing approaches fail? (2) Can Lttp verify the safety of
such programs efficiently?
We implemented Lttp as a verifier for programs represented in Java Virtual Machine (JVM) bytecode. The set of
benchmarks consists of some programs adapted from challenge benchmarks in the SV-COMP benchmark collection [20],
a program that cannot be verified by a competing approach [30], novel benchmarks designed to exhibit particular
capabilities of Lttp, and a program which demonstrates that Lttp is limited to properties that can be expressed in a
context free way.
In short, the results of our experiments indicate that Lttp can be applied to verify the safety of programs that
cannot be verified by existing shape analyzers or verifiers. The time required for the Lttp implementation to perform
verification varies dramatically, and we diagnose what causes intractability in some cases.
17

§6.1 describes our implementation of Lttp for JVM and our experimental procedure; §6.2 summarizes each benchmark;
§6.3 provide a qualitative evaluation of Lttp by describing the proofs that it synthesizes in order to prove the safety of
several illustrative benchmarks. §6.4 provides a quantitative evaluation of Lttp by analyzing its performance.

6.1

Implementation and experimental procedure

We implemented Lttp as a verifier for JVM bytecode. Lttp can thus be applied to verify programs written in Java, Scala,
or other languages with compilers that target the JVM. The hypothetical language, Lang, targeted by Lttp was defined
in §3.1, including classes of instructions that perform operations over objects, such as loads, stores, and allocations.
Each such instruction directly corresponds to an instruction in the JVM instruction set. In addition, the implementation
of Lttp can be applied to programs that use common operations over scalar data, such as linear arithmetic and Boolean
functions. Lttp does not currently support programs that consist of multiple procedures.
Lttp for JVM supports program specifications through library operations that implement the semantics of assume
and assert instructions. There are further operations for retrieving non-deterministic data. The semantics of Lang do
not include the concept of a NullPointerException or any other exception. Accessing the fields of a null object is
legal, undefined behavior in Lang. Lttp does not model exception-throwing runs of JVM programs. Even so, one can
verify the absence of a NullPointerException in the original program by injecting a null check before every field
access.
Lttp for JVM implements several optimizations, in comparison to the conceptual version of Lttp for Lang given
in §5. In particular, the performance of both the procedure SynGrammar for synthesizing a run grammar (§5) and
SolveCHC is heavily affected by the number of control locations of a given program. Lttp for JVM coalesces sequences
of value instructions, allocations, and control branches that are not loop back-edges a single block to reduce the number
of effective control locations. The benefit of this optimization is that SynSkeleton can represent the space of alternative
run-grammar skeletons more compactly, and SynGrammar can generate CHC systems with fewer relational predicates
and clauses. The disadvantage of this optimization is that the constraints in the generated CHC system are more
complex. In practice, the optimization results in a significant improvement in performance.
Furthermore, instead of modeling the value of each program variable at each control point using an uninterpreted
function (§4), Lttp translates the program into static single assignment form, and introduces first-order variables in
generated CHC systems that correspond to program variables. This increases the total number of first-order variables
included in a system, but allows the Lttp implementation to perform fixed-point analyses such as alias and object
liveness analysis that are relatively cheap compared to the performance cost of a CHC solver. Lttp runs such analyses
to simplify the constraints in the CHC clauses before solving.
Finally, on practical benchmarks, solving a given CHC system to obtain a counterexample is often far more expensive
than an explicit search through all possible program paths. Accordingly, before attempting to solve a given system, our
implementation of Lttp unrolls the system to enumerate all paths up to some heuristic depth and examines each one
with Alg. 2 to determine if it is a counterexample.
Lttp uses the Sawja program analysis framework [27] to process JVM bytecode input and the Z3 theorem prover [56]
to solve TD,Uif satisfiability queries (§3.2.1). Lttp uses as a CHC solver (§5) the implementation of Duality [9] that
accompanies Z3, modified to apply Z3’s aggressive formula simplifier after each iteration of its solving algorithm; The
original version of Duality performs only cheap simplifications, which often caused a problemtic explosion in the size
18

of the invariants. Lttp uses the XSB Datalog engine [52] to execute the fixed-point analyses for optimization prior to
solving. Aside from these components, the Lttp codebase consists of approximately 12,300 lines of OCaml.
We also implemented a baseline verifier for JVM bytecode which encodes programs using the theory of arrays to
model the heap. The baseline generates a CHC system with one relation for each control location and a clause for each
pair of adjacent control locations to model a step of execution. The heap of a program is modeled as a collection of
logical arrays, one for each field, that each map each object to the value stored at that field. Load and store instructions
are modeled with select and store operations of the theory of arrays, and objects are represented as integer identifiers.
In this way, the baseline reduces the problem of deciding program safety to the problem of solving a CHC system in
the theory of arrays with linear arithmetic, Auflia. The baseline verifier coalesces instructions similarly to Lttp as
described above, and attempts to solve the resulting system by running Duality.
We applied both the baseline and Lttp to a set of benchmarks to determine if Lttp could verify the safety of
programs that could not be verified using other theories that accurately model the semantics of memory operations.
For each benchmark program P, we gave P to Lttp and the baseline verifier and observed the result of, and resources
used by, each verifier to attempt to prove that P satisfies its single (without loss of generality) assert statement. For
most benchmarks, we discovered divergent behavior in the successive invariants generated by the baseline verifier so
that the solver would inevitably exceed any memory or time limits imposed. This behavior is reported as failure of the
baseline verifier.
We ran all experiments on a machine with 16 2.8 GHz processors and 16 GB of RAM. The current implementations
of Lttp and the baseline verifier execute using a single thread.

6.2

Description of benchmarks

The behavior of the thirteen benchmarks programs tested is as follows.
The benchmarks programs buildInspect, peel, unary, and binary perform similar tasks, but with increasing
complexity for Lttp. All four programs construct a singly-linked list (using a next field) from front to back, with some
property, and then proceed to scan the list from front to back, ensuring that the property holds. In buildInspect and
peel, the property to check is that the final non-null element scanned is indeed the final element that was added to the
list. In order to model the traversal of this list, Lttp must synchronize the matching iterations of the two loops, as
depicted in Figure 3. The grammar relations here each have two negative control pairs, representing control flow of the
two loops. While buildInspect has the list initialization peeled out of the fist loop, in peel Lttp must discover that
this peel is needed to match the iterations correctly. A data field is added to unary and binary. The first checks a
unary property over the entire list (that all data fields are zero), while the second checks a binary property (that the
integer data is increasing monotonically). A program like unary can be found in the SV-COMP benchmark collection.
The verification of allocator constitutes a demonstration that the encoding of unique object allocation is correct.
After an unbounded list is constructed on the heap, a final object o is allocated and subsequently compared to every
item in the list to check uniqueness.
lag2 constructs a list and scans it within the same loop. However, a given item is scanned exactly two iterations
after it is created.
An unbounded list ending with a fixed-length cycle is built by finiteCycle; it then scans this structure and fails
the assertion if the scan ever terminates.
19

Alternatively, breakCycle constructs a cycle of unbounded size and proceeds to consume it by destroying the next
pointers. Thus it asserts that the traversal terminates when it revisits the node from which it started. SV-COMP contains
a cycle-constructing program as well. However, the SV-COMP version of the program is fundamentally easier than
breakCycle because the data is never overwritten; the starting point is instead recognized by its integer data.
We adapted sameLength directly from a program given by Itzhaky et al. [30] which cannot be handled by effectively
propositional reasoning (EPR). The program simultaneously constructs two disjoint lists, and then simultaneously
scans them to check that they have the same length. This property relies on an invariant correlating the two disjoint
structures, which is not expressible by heap reachability (see §6.3).
The tree benchmark constructs a non-list data structure. Each element has two fields, a left pointer and a right
pointer. A loop non-deterministically allocates a left or right child for the last item allocated and maintains a counter
for the size of the structure. The program then follows the pointers to the end, and asserts that the same number of
nodes were traversed.
Two more SV-COMP benchmarks which we adapted are simpleSearch and uniqueItem. Our simpleSearch
constructs an unbounded list of consecutive integers of length at least 5, beginning with zero. It then expects to find the
integers 1 and 3. The original benchmark built a list of at least ten elements. Our uniqueItem constructs an unbounded
list with all data fields set to False, except for exactly one element, which has its data set to True. The program
then checks that there is one and only one such element. The original benchmark performed a more complicated
construction, wherein the unique element is inserted after the list is constructed.
The program named order constructs the first part of a list, of unbounded length, adds two distinguished list
elements a and b, then constructs the remainder of a list, of unbounded length. The scanning loop verifies that it does
not find b before finding a.
Finally, ctxSensitive behaves like lag2 in that the scanning of elements lags behind their construction in the
same loop. However, two elements are constructed and only one is scanned in each iteration. Incremental integer data
is stored with each element, and the program asserts that the data value in final element scanned is half of the data
value in the final element constructed.

6.3

Illustrative benchmark

In this section, we discuss in detail an additional benchmark and the operation of Lttp in verifying its safety.
A program with queues of equal length: sameLength. Figure 5 contains a program sameLength that builds two
queues simultaneously in a loop, then traverses the queues to check that they contain the same number of elements.
This benchmark was given in a previous study of Effectively Propositional Reasoning (EPR) in order to illustrate a class
of programs that techniques based on EPR cannot prove safe because their necessary invariants cannot be represented
in Effectively Propositional Logic (EPL) [29].
sameLength performs the following steps over an execution. sameLength first initializes two queues (lines 3—7).
In each iteration of the loop (lines 8—16, referred to as the building loop), sameLength adds an element to the tail of
each queue. sameLength non-deterministically chooses to exit the building loop It then traverses both queues, loading
one element in each iteration of a loop at lines 17—19, referred to as the traversal loop. sameLength exits the traversal
loop when it reaches the end of one of the queues. Finally, sameLength asserts that it has reached the end of both
queues (line 20).
20

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

class Element { Element next; }
public static void sameLength() {
Element head1 = new Element();
Element tail1 = head1;
Element head2 = new Element();
Element tail2 = head2;
boolean done = false;
while (!done) {
done = *;
Element tmp;
if (done) tmp = null;
else tmp = new Element();
tail1.next = tmp; tail1 = tmp;
if (done) tmp = null;
else tmp = new Element();
tail2.next = tmp; tail2 = tmp; }
while (head1 != null && head2 != null) {
head1 = head1.next;
head2 = head2.next; }
assert head1 == null && head2 == null; }

Fig. 5. sameLength: Constructs two queues in a loop where
each iteration adds one element to each queue, then traverses both in a second loop to show both queues have the
same length.

b:8

0

1

Loops
d:
17

2

3

Fig. 6. ctxSensitive: A program which Lttp cannot prove
safe.

Loops[0]

sameLength[0]
a:3

class Element { Element next; int data; }
public static void contextSensitive() {
Element head = new Element();
head.data = 0;
Element tail = head;
int count = 1;
while (*) {
Element tmp = new Element();
tmp.data = count;
tail.next = tmp; tail = tmp;
tmp = new Element();
tmp.data = count+1;
tail.next = tmp; tail = tmp;
head = head.next;
count = count + 2; }
assert head.data == count/2; }

c:
17

0
e:
20

Loops[1]

n:8

o:
17

0
2

1
3

0

c:
10

d:
12

j:
17

f:8

g:
14

h:8

0 1
Loops

2
k:
19

l:
17

2 3

i:
17

1
3
m:
20

Fig. 7. A graph grammar that generates sameLength’s control paths and data dependencies.

In order to prove that sameLength satisfies its assertion, a verifier must establish an invariant for the loop on lines
17—19 that expresses the fact that the lengths of both of the maintained queues are equal. Such an invariant cannot be
represented in EPL [29].
Figure 7 depicts a run grammar G that simulates and refutes sameLength, and is synthesized automatically by Lttp.
G contains two relational predicates, sameLength and Loops. The query relational predicate, sameLength, is the head
of one clause, sameLength[0]. The clause derives paths that step from the entry of sameLength to the entry of its
building loop (a—b), the step from the exit of the building loop to the entry of the traversal loop (c—d), and from the
exit of the traversal loop to the exit of the program (e).
The relational predicate Loops is the head of two clauses. Clause Loops[0] derives termination of both the building
and traversal loops. Clause Loops[1] derives simultaneous, data-dependent iterations of the building loop and traversal
loop. The clause derives a control path f—g in an iteration of the building loop up to its store that adds an element
to the first queue, a control path g–h from the store that adds to the first queue to a store that adds to the second
queue, a control path j—k that steps in a corresponding iteration of the traversal loop up to the load from the head of
21

Benchmark

allocator
binary
buildInspect
ctxSensitive
finiteCycle
lag2
order
peel
tree
sameLength
breakCycle
simpleSearch
unary
uniqueItem

Source

Novel

EPR
SVC

LoC

Iter

Rel

Cls

SynSkeleton
Time

SolveCHC
Time

Lttp

Base

22
29
22
21
19
24
32
25
38
28
25
33
26
36

3
7
5
–
8
4
7
8
4
2
10
6
6
4

7
13
7
–
8
9
14
10
11
11
13
12
12
11

13
19
13
–
15
13
24
16
16
17
21
18
18
17

17s
1h 13m 32s
19s
–
59s
20s
8h 19m 18s
7m 4s
41m 50s
23m 22s
5h 0m 46s
3h 19m 38s
56m 27s
33m 26s

4m 30s
5m 25s
1m 18s
–
1m 18s
6s
4h 10m 2s
7m 47s
16m 18s
7m 54s
55m 30s
5h 28m 15s
6m 41s
40m 10s

✓
✓
✓
–
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓

–
–
–
–
–
✓
–
–
–
–
–
–
–
–

Table 2. Results of our evaluation of Lttp. Information about the program source, features of the learned grammar, and execution
times of Lttp are reported. The columns of the table indicate the name of the benchmark (“Benchmark”), the source of the program
(“Source”), the number of lines of source code in the program (“LoC”), the number of iterations required to learn the final grammar
(“Iter”), the final number of relations and clauses in the final grammar (“Rel”, “Cls”), the total time spent in calls to the SynSkeleton
prototype, (“SynSkeleton Time”), the total time spent in calls to Duality (“SolveCHC Time”), and whether Lttp and the baseline
verifiers ultimately solved the verification problem (“Lttp”, “Base”).

the first queue, and a control path j—l that steps from the load from the head of the first queue to a load from the
head of the second queue. Figure 7 also depicts data dependencies from stores at instances of node g to corresponding
loads at instances of k and from stores at instances of h—l. As in previous examples, we omit rules which derive
non-corresponding steps of the loops, to simplify the presentation.
Loop is empty; one solution contains an interpretation of Loop as an invariant that establishes that the building loop
terminates if and only if both queues are null in a corresponding iteration of the traversal loop:
F(head, tail) ≡ tail0 = head2 ∧ next1 (tail0 ) = next2 (head2 ) =⇒ head3 = tail1
(done1 ⇐⇒ head13 = null ∧ head23 = null) ∧ F(head1, tail1) ∧ F(head2, tail2)

(2)

sameLength illustrates the ability of Lttp to prove safety of programs for which safety depends on properties that
relate disjoint unbounded, low-level data structures. Lttp does so by synthesizing invariants over relational predicates
that derive steps of execution that both load and store from related data structures. This ability enables Lttp to prove
the safety of programs that cannot be proved safe by existing techniques based on EPL [16, 29, 31]. These approaches
can prove properties expressed in terms of heap reachability within a linked list, but cannot verify properties that
require application-specific inductive definitions [29].
6.4

Results and analysis

The results of our evaluation are contained in Table 2. Each of the programs in Table 2 was proved safe by Lttp. Only
one of the benchmarks, lag2, was proved safe by the baseline verifier, which took three seconds.
SynSkeleton converges to the correct grammar after only 4 infeasible path examples in verifying buildInspect,
but requires 7 examples for convergence on peel. The SynSkeleton time for unary and binary is an order of
22

magnitude longer than for peel, which is in turn an order of magnitude longer than for buildInspect. This illustrates
the poor scalability of the constraint-based prototype as the program complexity increases.
Each time an object is allocated in allocator, the run grammar constraints can only ensure that the object is
distinct from a bounded number of other objects. Yet o is verified to be distinct from every element of the unbounded
list, indicating that the earlier allocations were aware of the eventual occurrence of o. This foresight is achieved because
the scanning of the list produces a grammar similar to that of buildInspect. Had the list not been scanned, o could
not be constrained to be distinct from the other elements, which is a safe approximation precisely because the list is not
scanned.
lag2 stands out as the only one which is determined to be safe by the baseline verifier, despite the fact that the
benchmark uses an unbounded heap structure. The baseline determines the program is safe in just three seconds. An
informal explanation is that though the entire structure is unbounded, only a bounded subset of it is live. The distance
between a store and its matching load is bounded at exactly two iterations of the loop. This special property permits the
invariants to be easily synthesized by Duality in the theory of arrays as a formula over a bounded number of indices.
This same property also manifests in Lttp, without the theory of arrays. The trivial first SynGrammar(P, ∅) result is
almost correct: a state variable must be kept in a relation for two iterations following its use in a control edge.
finiteCycle illustrates that Lttp can prove cyclicity of the visited control locations from the cyclicity of a data
structure.
Showing correctness of breakCycle depends on the ability of Lttp to accurately model a field which is written to
and read from more than once, with an unbounded number of heap modifications in between. If a verifier could not
prove that the nulled pointers remain null after traversing the unbounded cycle, there would be no guarantee of ending
at the correct element of the cycle.
Lttp is well-suited to verify sameLength, though it is inexpressible in EPR, because Lttp can capture correlations
between control flow and data movement in the structure of the CHC system.
Verifying tree shows that Lttp is not confined to lists since the data structure to be traversed proceeds nondeterministically through left and right child pointers.
Lttp solved simpleSearch, although its CHC system was the hardest one tested, taking 5.5 hours for Duality
to find inductive invariants. Because of the lower bound on the list size, the shortest of the feedback paths given to
SynSkeleton must execute the list construction step at least 5 times, since the vacuous refuting neighborhood is all
that is required to show infeasibility shorter paths. Moreover, it is speculated that the CHC solver must also explore
unwindings of the CHC system to that depth before meaningful invariants begin to be discovered.
Lttp is able to solve uniqueItem, illustrating its ability to model a program which can leave a special item at a
non-deterministic point in an unbounded list, and not only find it again, but prove that there is exactly one such item.
That Lttp can further solve order shows yet more expressivity in reachability conditions regarding multiple elements
in a list. A verifier would fail if it were only able to express that the elements a and b were reachable from the head of
list, and not that the elements are ordered.
ctxSensitive is unsolvable by both Lttp and the baseline verifier, despite its similarity to lag2, which both
verifiers performed very well on. Lttp did not synthesize a correct grammar no matter how many feedback paths it
received. The key difference from lag2 is that the distance between a load and its matching store increases with each
iteration. The limitation of Lttp in this case is discussed in below.

23

Limitations: While Lttp can verify a large class of programs which manipulate heap data structures, there are certain
types of programs which it cannot. In particular, the current implementation of Lttp is restricted to the subset of
programs which can be refuted using a context-free grammar.
Figure 6 contains the source code for a program, ctxSensitive, for which Lttp cannot synthesize a proof.
ctxSensitive constructs and consumes a queue in a single loop where each iteration appends two new elements
and consumes only one previous element. The program checks that the last element read was the middle element
written. First, the program initializes a queue with a single element and initializes a counter, count, to 1 (lines 3—6).
The program iterates an arbitrary number of times. In each iteration, two new elements are added to the tail of the
queue. The first element added has its data field set to count and the second has its data field set to count + 1 (lines
7—13). Then, the first element of the queue is removed by moving through the head’s next field (line 14). At the end
of each iteration count is incremented by 2 (line 15). Once the loop finishes, the program asserts that the data field of
the front of the queue is equal to half of the current value in count (line 16).
The problem with this benchmark is that the distance between corresponding stores and loads widens as the program
progresses. In other words, the data dependency is sensitive to the number of iterations of the loop that have occurred.
Therefore, the path-grammar required to describe the data dependencies of ctxSensitive is not context-free.
Non-context-free grammars are a fundamental limitation of the presented approach. Extending our technique with
the capability of handling more complex grammars is a compelling direction for future work.

7

RELATED WORK

Three-valued logic analysis (TVLA) represents sets of program heaps as canonical structures [35, 41, 45]. Recent work has
introduced automatic shape analyses that represent sets of program heaps as formulas in separation logic [12, 15, 42, 53],
forest automata [26], or memory graphs [17]. Lttp can be applied to programs that maintain perform arbitrary low-level
heap operations and data operations. Such approaches can potentially infer invariants of heaps that maintain a variety
of data structures, such as lists or trees. However, each analyses synthesizes invariants using an abstraction fixed for
the run of the analysis: thus, the analysis can only potentially be effective if an analysis designer provides a sufficient
set of predicates for maintaining invariants required to prove that a program satisfies a desired property. Variants of
TVLA have been extended to automatically refine an abstraction used by applying Inductive Logic Programming (ILP).
However, previous work has established only have ILP can be applied to refine structural abstractions, not abstractions
over structure and data.
Recent work has also proposed decision procedures for separation logic [39, 46] and an automatic verifier that
represents sets of states as separation-logic formulas [1]. Such approaches require a fixed set of recursively-defined
predicates for reasoning about fixed classes of heap data structures. Lttp can verify program correctness without
requiring such predicates.
Previous work has developed automatic verifiers that implement predicate abstraction in shape logics. Such approaches can only synthesize invariants that describe which cells of a heap may reach each other over heap fields [4, 14],
can be applied only to programs that maintain particular data structures—such as linked lists [34]—or require an
analyst to provide loop invariants [10], predicates over which invariants are constructed [19, 40, 43], or heuristics that
ensure that the analysis converges [14]. Relational invariants of path grammars can prove correctness of programs
that maintain non-list data structures. Lttp can potentially synthesize such invariants without requiring an analyst to
provide predicates or loop invariants.
24

Previous work has proposed verifiers that determine if a program satisfies an assertion by inferring shape invariants
represented as formulas in effectively-propositional logics [16, 29, 31]. Such verifiers enjoy strong completeness
properties not satisfied by Lttp, but the class of invariants that they synthesize cannot express invariants over non-list
data structures or that relate multiple lists. Relational invariants over path grammars can prove the safety of programs
that maintain such data structures, and Lttp can potentially synthesize such invariants automatically.
One such verifier [31] is in fact one instance of a verification framework that could potentially be instantiated
with logics other than effectively-proposition logics. However, the general framework requires an analyst to provide
predicates over which verification is to be performed. Lttp does not require such predicates to be provided.
Further work on effectively-propositional logic describes a verifier that can verify properties of heap-paths of
data-structures that are not necessarily lists [28]. However, the verifier requires pre-conditions and post-conditions to
be given explicitly. It cannot verify programs with loops, although loops annotated with invariants could presumably
be verified by directly adapting the verification technique. In either case, Lttp is distinct from the verifier in that Lttp
can potentially prove safety of an iterative program automatically.
Previous work has described verifiers that verify that a given program satisfies a desired shape property by axiomatizing and inferring invariants in the theory of arrays. One approach attempts to infer invariants that are quantified
over array indices and use range predicates that describe the values at different ranges of indices in an array [33].
Such invariants are well-suited to inferring invariants that describe logical arrays that model arrays operated on by a
program, but not logical arrays that model a program’s heap fields.
Previous work has proposed approaches that attempt to verify a given program by synthesizing a tree-decomposition
of the heaps that it maintains [36, 37]. Lttp is similar to such approaches in that it reasons about tree-structured
artifacts that model program executions, namely the derivation trees of a grammar of program paths. Unlike previous
approaches, Lttp reasons about the derivation of control paths, rather than of a decomposition of the heap.
Techniques from relational verification [6–8] establish properties over states in multiple runs of a program, such as
robustness and information-flow security, or over states in runs of multiple programs, such as observational equivalence.
Lttp can be viewed as an instance of relational verification, in that it attempts to synthesize proofs that establish
properties over multiple states. Lttp is distinct from previous work in that it attempts to establish properties of
states within the same run in order to prove safety of low-level programs. Combining existing relational verification
techniques with Lttp in order to prove relational properties of programs that maintain low-level data structures and to
automate relational verification seems to be a promising direction for future work.
Sketch synthesizes finite programs [50], bit-streaming programs [50], and stencils [47] by iteratively synthesizing a
candidate version of a program, attempting to verify it, and using a counterexample to verification to guide the search
for the next version of the program. Synthesizers that are instances of the SyGuS framework [2] attempt to synthesize
a program accompanied with a proof of correctness, using a counterexample-guided, iterative process. Lttp is similar
to Sketch and instances of SyGuS in that it is an inductive synthesizer. Lttp is distinct from Sketch and instances of
SyGuS in that each of them, given a partially-complete program, attempt to complete the program with instances of a
language of possible syntactic combinations of atomic operations. Lttp, given a program P, attempts to synthesize the
basic structure of a logic program that simulates P, without synthesizing new atomic operations.
Previous work has reduced the problem of verifying concurrent programs that use a bounded number of threads
to solving a system of Constrained Horn Clauses (CHC’s) [22] and proposed a solver for CHC’s over the theory of
linear arithmetic. Previous work has developed automatic verifiers for programs with a single procedure [38] and
25

multiple recursive procedures [23] that have been generalized to design CHC solvers that use an interpolating theorem
prover [9, 44]. Lttp uses a CHC solver for the theory of uninterpreted functions as a black box. In principle, Lttp can
use any CHC solver; the implementation evaluated uses a solver that itself uses an interpolating theorem prover [9].
8

CONCLUSION

In this paper, we have presented a novel verifier, named Lttp, designed to verify programs that maintain low-level
data structures. The key feature of Lttp is that, given a program P, it attempts to synthesize a proof of the safety of P,
represented as a graph grammar, i.e. a CHC system, that generates the control paths of P, annotated with invariants
that relate the local values at multiple points in each path. Lttp is completely automated, using an inductive-synthesis
algorithm that synthesizes candidate path grammars by reduction to constraint solving and validates candidate grammars
by reduction to logic programming. Such proofs can establish correctness of programs that previously could only be
proven correct using manually-provided predicates over values and structure.
We have implemented Lttp as a verifier for JVM bytecode and evaluated it on a set of challenging problems for
shape verifiers. Lttp for JVM succeeded in learning a suitable grammar for thirteen of the fourteen benchmarks. Each
of the suitable grammars was given as a CHC system to the CHC solver Duality, which was able to find inductive
invariants to prove program safety.
The design of Lttp establishes that shape-verification problems can potentially be solved by applying techniques from
relational verification and inductive synthesis. Further work strengthening this connection could result in significant
development of each of the related fields.
ACKNOWLEDGMENTS
This work is supported by the National Science Foundation under awards 1526211 and 1650044.
REFERENCES
[1] A. Albarghouthi, J. Berdine, B. Cook, and Z. Kincaid. Spatial interpolants. In ESOP, 2015.
[2] R. Alur, R. Bodı́k, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided
synthesis. In FMCAD, 2013.
[3] D. Angluin. Learning regular sets from queries and counterexamples. InfComp, 75(2):87–106, 1987.
[4] I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI, 2005.
[5] T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54(7), 2011.
[6] G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In FM, 2011.
[7] G. Barthe, J. M. Crespo, and C. Kunz. Beyond 2-safety: Asymmetric product programs for relational program verification. In LFCS, 2013.
[8] N. Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL, 2004.
[9] N. Bjørner, K. L. McMillan, and A. Rybalchenko. On solving universally quantified horn clauses. In SAS, 2013.
[10] C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. C. Rinard. Using first-order theorem provers in the jahob data structure verification system. In
VMCAI, 2007.
[11] F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In Formal Methods, pages 128–141, 1993.
[12] C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6), 2011.
[13] A. Clark. Distributional learning of some context-free languages with a minimally adequate teacher. In ICGI, volume 6339, pages 24–37, 2010.
[14] D. Dams and K. S. Namjoshi. Shape analysis through predicate abstraction and model checking. In VMCAI, 2003.
[15] D. Distefano, P. W. O’Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, 2006.
[16] S. Drews and A. Albarghouthi. Effectively propositional interpolants. In CAV, 2016.
[17] K. Dudka, P. Peringer, and T. Vojnar. Byte-precise verification of low-level list manipulation. In LNCS, 2013.
[18] C. Flanagan. Automatic software model checking using CLP. In ESOP, 2003.
[19] C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL, 2002.
[20] Github - sosy-lab/sv-benchmarks: svcomp17. https://github.com/sosy-lab/sv-benchmarks, 2017. Accessed: 2017 July 1.
[21] S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, 2011.

26

[22]
[23]
[24]
[25]
[26]
[27]
[28]
[29]
[30]
[31]
[32]
[33]
[34]
[35]
[36]
[37]
[38]
[39]
[40]
[41]
[42]
[43]
[44]
[45]
[46]
[47]
[48]
[49]
[50]
[51]
[52]
[53]
[54]
[55]
[56]

A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, 2011.
M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, 2010.
T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004.
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002.
L. Holı́k, O. L. O, A. Rogalewicz, J. Šimáček, and T. Vojnar. Fully automated shape analysis based on forest automata. In CAV, 2013.
L. Hubert, N. Barré, F. Besson, D. Demange, T. P. Jensen, V. Monfort, D. Pichardie, and T. Turpin. Sawja: Static analysis workshop for Java. In
FoVeOOS, 2010.
S. Itzhaky, A. Banerjee, N. Immerman, O. Lahav, A. Nanevski, and M. Sagiv. Modular reasoning about heap paths via effectively propositional
formulas. In POPL, 2014.
S. Itzhaky, A. Banerjee, N. Immerman, A. Nanevski, and M. Sagiv. Effectively-propositional reasoning about reachability in linked data structures.
In CAV, 2013.
S. Itzhaky, A. Banerjee, N. Immerman, A. Nanevski, and M. Sagiv. Effectively-propositional reasoning about reachability in linked data structures.
Technical report, Tel Aviv University, 2013.
S. Itzhaky, N. Bjørner, T. W. Reps, M. Sagiv, and A. V. Thakur. Property-directed shape analysis. In CAV, 2014.
S. Izhaky, S. Gulwani, N. Immerman, and M. Sagiv. A simple inductive synthesis methodology and its applications. In OOPSLA, 2010.
R. Jhala and K. L. McMillan. Array abstractions from proofs. In CAV, 2007.
S. K. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. In POPL, 2006.
A. Loginov, T. W. Reps, and S. Sagiv. Abstraction refinement via inductive learning. In CAV, 2005.
R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graph decomposition. In TACAS, 2007.
R. Manevich, T. Lev-Ami, M. Sagiv, G. Ramalingam, and J. Berdine. Heap decomposition for concurrent shape analysis. In SAS, 2008.
K. L. McMillan. Lazy abstraction with interpolants. In CAV, 2006.
J. A. N. Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, 2011.
Z. Rakamaric, J. D. Bingham, and A. J. Hu. An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable
data and cyclic data structures. In VMCAI, 2007.
T. W. Reps, S. Sagiv, and R. Wilhelm. Static program analysis via 3-valued logic. In CAV, 2004.
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.
P. M. Rondon, M. Kawaguchi, and R. Jhala. Low-level liquid types. In POPL, 2010.
P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for horn-clause verification. In CAV, 2013.
S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24(3), 2002.
S. A. Seshia, S. K. Lahiri, and R. E. Bryant. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In DAC, 2003.
A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodı́k, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, 2007.
A. Solar-Lezama, C. G. Jones, and R. Bodı́k. Sketching concurrent data structures. In PLDI, 2008.
A. Solar-Lezama, R. M. Rabbah, R. Bodı́k, and K. Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI, 2005.
A. Solar-Lezama, L. Tancau, R. Bodı́k, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006.
S. Srivastava, S. Gulwani, S. Chaudhuri, and J. Foster. Path-based inductive synthesis for program inversion. In PLDI, 2011.
Xsb datalog. https://http://xsb.sourceforge.net/, 2017. Accessed: 2017 July 1.
H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O’Hearn. Scalable shape analysis for systems code. In CAV, 2008.
R. Yoshinaka. Towards dual approaches for learning context-free grammars based on syntactic concept lattices. In Developments in Language Theory,
pages 429–440, 2011.
R. Yoshinaka and A. Clark. Polynomial time learning of some multiple context-free languages with a minimally adequate teacher. In Formal
Grammar, pages 192–207, 2012.
Z3prover/z3 - github. https://github.com/Z3Prover/z3, 2017. Accessed: 2017 July 1.

27

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

class Element { Element next; }
enum St { W, RW, R, DONE; }
public static void lag() {
Element head = new Element();
Element tail = head;
St s = St.W;
while (s != St.DONE) {
if (s == St.W || s == St.RW) {
Element tmp = new Element();
tail.next = tmp;
tail = tmp; }
if (s == St.RW || s == St.R) { head = head.next; }
if (s == St.W) { s = St.RW; }
else if (s == St.RW && *) { s = St.R; }
else if (s == St.R) { s = St.DONE; } }
assert head == tail; }

Fig. 8. lag: Constructs and consumes a queue, with each load
occurring one iteration after the corresponding store.

c:
12

d:7

1

Loop[1]

k:
12

0
Loop

a:3

Fig. 9. order: Constructs and queue with two distinguished elements. It then consumes the queue to
ensure the distinguished elements remain in the order
they were inserted.

Loop[0]

lag[0]
b:7

class Element { Element next; }
public static void order() {
Element head = new Element();
Element tail = head;
while (*) {
Element tmp = new Element();
tail.next = tmp; tail = tmp; }
Element a = new Element();
tail.next = a; tail = a;
Element b = new Element();
tail.next = b; tail = b;
while (*) {
Element tmp = new Element();
tail.next = tmp; tail = tmp; }
boolean ordered = true;
while (head != a) {
if (head == b) ordered = false;
head = head.next; }
assert ordered; }

2

0
1

0
e:
16

g:7

2
m:
16

l:7

h:
12

1
0
f:
12

0
Loop

i:7

1

2

2
j:
16

Fig. 10. A graph grammar that generates lag’s control paths and data dependencies.

A

ADDITIONAL ILLUSTRATIVE BENCHMARKS
A program with nodes shared across clauses: lag. Figure 8 contains the source code for a program, lag, which builds and consumes

a queue. Both the loads and stores occur in a single loop, where each item that is loaded was stored on the previous iteration. The
program operates in the context of a small state machine. First, lag initializes the queue and sets itself in a write-only state (lines
4—6). Next, if lag is in a write state, then it adds a new element to the end of the list and sets the tail to this new element (lines 7—11).
If lag is in a read state, it moves the head to the next element (line 12). lag then performs state transitions (lines 13—15). lag moves
from the write-only state to the read-write state and from the read-only state to the done state after a single iteration. lag moves from
the read-write state to the read-only state after an arbitrary number of iterations. Finally, lag asserts that the head element reached by
this loop is the same as the tail (line 16).
Figure 10 depicts a graph grammar, G, which describes the control paths and data dependencies of lag. The grammar contains
two relations, lag and Loop, where lag is the query relation. G has three clauses. lag[0] generates fragments of the control path
which describe the loop entry (a—b), through the first store (b—c), and through the first state transition without performing a load
(c—d). Loop[0] generates fragments of the control path which store the next item in the queue (g—h), load the front of the queue, and
perform a state transition (h—i). In addition, Loop[0] contains a data dependency (f—i): The store from the previous loop iteration

28

Loop0[0]

order[0]
a:3

b:5

0

1

Loop0

2
h:
19

c:8

0

g:
16

2

3

0

1

d:
12

Loop1

3

1

f:
16

e:
15

Loop0[1]

o:5

p:8

i:5

j:5

0

1

0

2

3

2

q:
16

r:
16

l:
16

0

Loop1[0,1]
1

Loop0
m:
16

2

3

k:8

v:
12

0

1

1
3

0

n:
16

s:
12

Loop1
t:
12

0

1

w:
15

1
u:
15

Fig. 11. A graph grammar that generates order’s control paths and data dependencies.

provides the data for the load in this iteration. Loop[1] generates the final fragment which skips from the beginning of the loop to just
after the loop (l—m).
A noteworthy feature of G is node f. In particular, f provides a data dependency, but is not connected directly to the control path
through Loop[0]. This demonstrates the capability of graph grammars to separate data dependencies from control dependencies.
A program for which some heap operations have no data dependencies: order. Figure 9 contains the source code for a program,
order, which creates a queue with two distinguished elements, then consumes the queue until it can check these two elements remain
relatively ordered. First, order initializes the queue and adds an arbitrary number of elements to the tail (lines 3—7). Next, it inserts
two distinguished elements, a and b (lines 8—11). order continues to expand the queue with an arbitrary number of new elements
(lines 12—14). order traverses the queue until it reaches element a. If b is encountered before the end of this loop, then the queue has
become unordered (lines 15—18). Finally, order asserts that the distinguished elements remain in order (line 19).
Each execution of order satisfies the assertion. The key invariant which could prove the safety property establishes that for each
iteration of the loop on lines 12—14, traversing the next pointer reaches a before it reaches b. This invariant is difficult to express
without knowing particular facts about the relationships of linked lists. However, a graph grammar can express the idea of this
invariant by simulating the first and third program loops together.
Figure 11 depicts a graph grammar, G, which encodes order. G has three relations and five clauses. The query relation, order, has
only one clause, order[0], which contains the entry to the first program loop (a—b), the insertion of the two distinguished elements
and entry of the second loop (c—d), the entry to the third loop (e—f), a final execution of the third loop and the program assertion
(g—h), and a data link between the first distinguished element and the final load (d—h). The two clauses of Loop0, Loop0[0] and
Loop0[1], describe the simultaneous execution of the first and third program loops. These clauses are similar to StLd[0] and StLd[1]
from §2.2.1. The two clauses of Loop1, Loop1[0] and Loop1[1] describe the execution of the second program loop. For brevity, we
omit some clauses for Loop0 that iterate the two loops a differing number of times. We annotate Loop0 with an inductive relational
invariant which can prove the safety of order:
tail1 , a2 ∧ head3 = tail1 ∧ ordered3 ∧ tail0 = head2 ∧
next1 (tail0 ) = next2 (head2 ) =⇒ head3 = tail1

(3)

This invariant maintains that the flag ordered is always true at the end of third loop. In addition, it establishes that the simultaneous
iteration of the first and third loop terminates before the distinguished element a is reached. Interestingly, the second loop is irrelevant
to proving the safety property, so the relational invariant for Loop1 is simply t r ue.
Previous examples have all contained data dependencies for every store and load. order demonstrates that this is not a limitation of
Lttp. The stores performed in the second program loop have no corresponding loads. This is reflected by the lack of data dependencies
in the clauses of the relation Loop1.

29

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

class Tree { Tree left; Tree right; }
public static void tree () {
Tree root = new Tree();
Tree t = root;
int c = 0;
Tree l,r,tmp;
while (t != null) {
c++;
if (*) tmp = new Tree();
else tmp = null;
if (*) l = tmp; r = null;
else l = null; r = tmp;
t.left = l; t.right = r;
t = tmp; }
t = root;
int d = 0;
do {
d++;
l = t.left; r = t.right;
if (l != null) t = l; else t = r;
} while (l != null || r != null);
assert c == d; }

Fig. 12. tree: Constructs a tree by arbitrarily adding left or right nodes, then follows the path to ensure the length when consumed
is the same as the length of the constructed path.

A program with a tree data structure: tree. Figure 12 contains a program, named tree, that constructs a tree data structure.
tree builds the tree by non-deterministically choosing to continue to build the left or right subtree of a given node for a nondeterministically chosen number of iterations. tree then traverses the data structure and ensures that the number of steps taken to
traverse it is the same as the number of steps used to build it.
In particular, tree enters the loop in lines 7—14 (i.e., it’s building loop) by initializing the tree and initializing a counter c of the
number of nodes. Before each iteration of the loop, tree tests if the tree node bound to t is null, and if so, exits the loop (line 7). In
each iteration of the loop, tree increments c (line 8) and non-deterministically chooses whether to stop adding new nodes (lines
9—10). The new node is then stored in either the left or right field of the node bound to t (lines 11—13).
After executing the loop, tree binds t to the root of the build tree (line 15) and initializes a new counter d to 0 (line 16). When
tree executes the loop on lines 17—21 (i.e., its traversal loop), it traverses the constructed path by loading either the left or right
child of a node maintained in t, depending on which child is not null (lines 17—20). tree executes its traversal loop until it reaches
a node such that both children are null (line 21). tree then asserts that the number of nodes added is the same as the number of
nodes traversed (line 22).
tree satisfies the safety property tested by its assertion at line 22 However, the loop invariants required to prove the property must
express a complex property that relates data structure and values. Such invariants must establish that the tree contains c elements
while tree executes the loops in lines 7—14, and that c − d elements are reachable from the object in t while tree executes the loop
in lines 17—21. To our knowledge, no automated invariants can synthesize proofs in a language that can express such properties.
Figure 13 depicts a run grammar G that simulates and refutes tree. G contains two relational predicates, tree and Loops. The
query relational predicate, tree, is the head of clause tree[0]. Clause tree[0] derives a control path that steps from program entry to
the entry of tree’s building loop (a—b), a path that steps from the exit of the building loop to the entry of the traversal loop (c—d),
and a path that steps from the exit of the traversal loop to the assertion (e).
Loops is the head of three different clauses. Clause Loops[0] derives steps in which the building loop non-deterministically chooses
to exit; in the corresponding step of traversal loop, it determines that it has reached the end of the tree. Clause Loops[1] derives
simultaneous steps of both loops such that the building loop chooses to build a subtree from the left field of the maintained tree
node. f—g derives a path through the building loop, while i—j depicts the corresponding path through the traversal loop. Each path
point derived as an instance of g is a data dependence of the node derived as an instance of j in the same clause instance, depicted by
the data-dependence edge from g to j. Clause Loops[2] is similar to Loops[0], but derives corresponding steps of both loops in which
the building loop builds a tree at the right field of the maintained tree node. Similar to the presentation of buildInspect in §2, we

30

Loops[0]

tree[0]
a:3

b:7

0

1

c:
15

Loops[1]

r:7

s:
15

f:7

0

1

0

g:7

2

3

0

2

3

2

e:
22

t:
17

u:
22

o:
17

1

left Loops

Loops
d:
17

0

Loops[2]

p:
17

2

3

n:
13

l:7

1

0

3

2

q:
22

o:
17

m:
7

0

1

right Loops
p:
17

2

3

n:
13

1
3
q:
22

Fig. 13. A graphical depiction of a run grammar that simulates and refutes tree. Control and data dependencies between path
points are depicted similarly to Figure 3.

have omitted clauses that derive extraneous iterations of either the building or traversal loops. Such clauses are necessary to represent
a run grammar that simulates all control flow paths of tree, since it is not known a priori that every execution has an equal number
of iteration in each loop.
G simulates tree and is empty; one solution of G includes an interpretation of Loops as a relational invariant that establishes that
c and d have the equal values at the end of iterations on which they store to and load from the same field:
lrnull(ix 0, ix 1) ≡ lefti x 0 (ti x 1 ) = null ∧ righti x 0 (ti x 1 ) = null
c1 = d3 ∧ (lrnull(1, 0) ⇐⇒ lrnull(2, 2))

(4)

In this invariant we define a formula macro lrnull over two indices which specifies that the left and right fields of the variable t
are both null at the given indices. To our knowledge, no automatic shape verifier developed in previous work can prove the safety of
tree without being guided to use a manually-defined recursive predicate that describes the shape of trees, and relevant predicates
over data variables c and d. However, Lttp can prove the safety of tree automatically.
B

IMPLEMENTING SYNSKELETON BY REDUCTION TO CONSTRAINT SOLVING

We now formalize some concepts that will assist in proving the lemmas and explaining more precisely how the constraints used
to implement SynSkeleton work. In the following sections, let a program P ∈ Lang be given. Let C be a CHC system, and let
the space to which C belongs be denoted CHCsR, X . Assume, without loss of generality, that the arity of every R ∈ R is n. Let
Idxs = {i ∈ N | i ≤ n }. Let α (Y, i) be the ith item in the sequence Y for Y ∈ X n and i ∈ Idxs. Further, for every control location
l ∈ Locs[P], let Ll be a unary interpreted function. Further, let Ctrl, Data, and Conn be binary uninterpreted functions.
Location consistency. Suppose there exists λ̂ : R × Idxs → Locs with the following property for all clauses C = (B, φ, H ) ∈ C, all
applications (R, Y ) ∈ B ∪ {H }, and all indices i ∈ Idxs:
Û
φ |=
(l = λ̂(R, i) ⇐⇒ Ll (α (Y, i))).
l ∈Locs
Then C is location consistent. Also define the map λ̂C : X → Locs for each clause C = (B, φ, H ) ∈ C such that if φ |= Ll (x ) then
λ̂C (x ) = l , for all variables x ∈ X and locations l ∈ Locs. λ̂C is well-defined because C is location consistent.
Control consistency. Suppose C is location consistent. Let λ̂C be given for all clauses C ∈ C. Suppose there exists ÊC ⊆ X × X for
each clause C = (B, φ, H ) ∈ C with the following properties for all variables x 1, x 2 ∈ X :
(1) If there does not exist an instruction Instr[P](λ̂C (x 1 ), λ̂C (x 2 )), then φ |= ¬Ctrl(x 1, x 2 );
(2) φ |= ÊC (x 1, x 2 ) ⇐⇒ Ctrl(x 1, x 2 ).
Then C is control consistent.

31

Path consistency. Suppose C is control consistent, and let ÊC be given for all clauses C ∈ C Suppose there exist a total ordering
< R over Idxs and a map sgnR : Idxs → {+, −} for every relation R ∈ R, such that the following properties hold for all clauses
C = (B, φ, H ) ∈ C, all applications (R 1, Y1 ), (R 2, Y2 ), ∈ B ∪ {H }, all indices i, j, k ∈ Idxs, and all variables x 1, x 2, x 3 ∈ X :
(1) If (α (Y1, i), α (Y2, j)) ∈ ÊC then φ |= Conn(α (Y1, i), α (Y2, j)) and
(a) if also (R 1, Y1 ) = H then φ |= sgnR 1 (i) < 0,

(b) if also (R 1, Y1 ) ∈ B then φ |= sgnR 1 (i) > 0;

(2) If (α (Y1, i), α (Y2, j)) < ÊC and if φ |= α (Y1, i) = α (Y2, j) then sgnR 1 (i) = sgnR 2 (j);

(3) φ |= Conn(x 1, x 2 ) ∧ Conn(x 2, x 3 ) =⇒ Conn(x 1, x 3 );
(4) φ |= i < R 1 j ⇐⇒ Conn(α (Y1, i), α (Y1, j)).
Then C is path consistent.

For a path consistent C, define sets of index pairs ⇝+R and ⇝−R for each relation R ∈ R as follows. Let ⇝+R = {(i, j) | sgnR (i) >

0 ∧ i < R j ∧ k ∈ Idxs(i < R k < R j)} ⊆ Idxs × Idxs. Define ⇝−R similarly, but with sgnR (i) < 0. The sets ⇝+R and ⇝−R are the
positive and negative control pairs of R, respectively. Informally, at any node d of any derivation tree D of C, with head (R, Y ), the
control path between α (Y, i) and α (Y, j) is constructed entirely within the subtree of D rooted at d if i ⇝−R j. Similarly, the control

path is constructed entirely outside of the subtree of D rooted at d if i ⇝+R j. For convenience, define the application of ⇝+R to

variable tuple Y ∈ X n as the set of variable pairs ⇝+R (Y ) = {(α (Y, i), α (Y, j)) | i ⇝+R j, i, j ∈ Idxs} ⊆ X × X . Define ⇝−R (Y )
similarly.
Neighborliness. Let C be such that for each C ∈ C and all x 1, x 2 ∈ X ,
φ |= Data(x 1, x 2 ).
Then C is neighborly.

Completeness and Correctness. If every path p ∈ Paths[P] is induced as the control graph of some model of C, then C is complete
for P.
Let p ∈ Paths[P] be infeasible. If each derivation of C that induces p as a control graph also induces a ν a refuting neighborhood of
p, then C is correct for p. If C is complete for P and correct for all infeasible paths p ∈ Paths[P], then C is correct for P.
There is a direct correspondence between the models m ⊢ SymPath(P, p, ν All ) and runs of p. Model m corresponds to run (p, σ )
with σ defined by σ (n) = (γ n , U n ), where γ n (a) = m(a(σn )) and U n (f, x) = n ′ where m(f(tnow (σn ), x(σn ))) = m(tnow (σn ′ )) if
any such n ′ exists, for all n ∈ N , a ∈ Vars, x ∈ OVars, f ∈ Fields.
Generating a skeleton from constraint solutions. The prototype implementation of SynSkeleton is a constraint-based approach to
grammar synthesis. We encode a space G of grammars using uninterpreted functions to model the structure of relations and clauses.
With loss of generality, the prototype only considers linear grammars, in the sense that every clause has at most one relation in the
body. Lttp has been formulated for only single procedure programs, whose control flow can be described linearly, and a need for
non-linear grammars has not yet been encountered in Lttp. The prototype also requires as input a budget specifying the maximum
arity of relations and the maximum number of relations for systems in G. This configuration is encoded as the set of constants and
uninterpreted functions of an SMT query.
The following properties of every C ∈ G are achieved by SMT constraints:
(1) Location consistency: This gives rise to λ̂C : X → Locs for each clause C.
(2) Control consistency: WLOG, each clause C entails exactly one control edge, i.e., ÊC = {(a, b)}.
(3) Path consistency: The arguments of every relation are partitioned into some number of negative control pairs and some
number of single auxiliary variables. Let (R 2, φ, R 1 ) be a clause. Under path consistency, R 1 is responsible for completing the
control paths between its negative pairs, and R 2 inherits what is not explicitly completed by R 1 . Assume that R 1 constructs
the control edge (a, b) between negative pair (a ′, b ′ ). If (a, b) = (a ′, b ′ ), then this pair is completed and a, b become

32

auxiliary variables in R 2 . If b , b ′ , then only a ′ becomes auxiliary and a ⇝−R b ′ . Likewise for a , a ′ . If both a , a ′ and
2

b , b ′ , then the control pair is split in two in R 2 : a ′ ⇝−R a ⇝+R b ⇝−R b ′ . Auxiliary variables (those not in any negative
2

2

2

pair) may or may not be forwarded to R 2 . In the general case, for x ⇝+R y ⇝+R z, when y is not forwarded, x ⇝+R z.
1

1

2

(4) Completeness as a path grammar: For each clause with control edge (a, b), λ̂C (a) is uniquely determined by the head
relation. For each relation R, there is (at least) one clause with head R for each possible value of λ̂C (b). The query relation
contains the unique (WLOG) initial and final control locations as a negative control pair. By induction over the clauses, each
R completes all possible paths between every negative control pair.
(5) Unambiguity (with loss of generality): For each relation R, there is at most one clause with head R for each possible value of
λ̂C (b), guaranteeing that every control path p has a unique derivation.
(6) Correctness for a path p ∈ F : A collection of uninterpreted functions witnesses a derivation of p by the grammar and further
witnesses that the neighborhood ν = Deps(P, p) is achieved, assuming neighborliness. That this holds for all derivations of p
is trivial with unambiguity.
C

PROOFS OF LEMMAS AND THEOREMS
Lemma 1. If P is simulated by S and P is refuted by S, then P is safe (§3.1.2).
Proof. S has no model that is a run P, by the assumption that P is refuted by S. Therefore P has no run by the assumption that P

is simulated by S. Thus P is safe, by the definition of safety (§3.1.2).

□

Lemma 2. If p is a feasible path of P, then IsFeas(P, p, ν All ) = True. Otherwise, IsFeas(P, p, ν All ) = False.
Proof. Sketch. IsFeas uses the formula SymPath(P, p, ν All ), which is a conjunction of constraints which precisely model the
semantics of each instruction in p. Notably, for every load there is at most one matching store. Every load is constrained with the
value of its matching store since the neighborhood ν All allows for every control state of p to be examined in search of the unique
match. Thus, the semantics of Lang are not approximated, and SymPath(P, p, ν All ) is satisfiable exactly when p has a run.

□

Lemma 4. Let p = (N , λ, E) ∈ Paths[P] and a neighborhood ν 0 : N → P(N ) be given. SymPath(P, p, ν 0 ) |= SymPath(P, p, ν All ).
Proof. SymPath(P, p, ν ) is a conjunction of constraints modeling the instruction on each edge (u, v) ∈ E, which is SymRel[i](u, v, ν (v))
for the instruction i = Instr[P](λ(u), λ(v)). For every n ∈ N , ν 0 (n) ⊆ ν All (N ) = N . We have that SymRel[i](u, v, ν 0 (v)) |=
SymRel[i](u, v, N ), shown case-wise for every possible instruction i:
• If i ∈ InstrsV , then SymRel[i](u, v, Q ) does not depend on the set of states Q .
• If i ∈ Stores ∪ Loads ∪ Allocs, then SymRel[i](u, v, Q ) takes only a conjunction over the q ∈ Q . Since ν 0 (v) ⊆ N ,
SymRel[i](u, v, ν 0 (v)) is no stronger than SymRel[i](u, v, N ).
Since SymPath is only a conjunction of SymRel constraints, SymPath(P, p, ν 0 ) cannot be any stronger than SymPath(P, p, ν All ). □
Lemma 5. Let a control path p = (N , λ, E) ∈ Paths[P] and any neighborhood graph (N , E Data ) be given. Let ν : N → P(N ) be the
neighborhood induced by (N , E Data ). Suppose p with ν are modeled by some derivation D of a skeleton C. Let G be the run grammar
corresponding to C. Then there is a model of D in G iff there is a model of SymPath(P, p, ν ).
Proof. Let a model of D in G be given as (D, m D , i), where m D is a model of the background theory and i : Nodes[D] →
Models[X ] maps derivation nodes to models of the CHC variables X . Since C, a skeleton, is control consistent by the specification
of SynSkeleton, every control edge (u, v) ∈ E = m D (Ctrl) via the constraint φ of the clause C of some node d in D, as follows:
Let λ̂C , ÊC be given. There exists a pair (x 1, x 2 ) ∈ ÊC such that i(d )(x 1 ) = u, i(d )(x 2 ) = v and φ |= Ctrl(x 1, x 2 ). There is a
corresponding clause in G with a constraint ψ |= φ. Moreover, because ψ |= SymRel[Instr[P](λ̂C (x 1 ), λ̂C (x 2 ))](x 1, x 2, X ), and
because G is location consistent and neighborly, i(d ) ⊢ SymRel[Instr[P](λ(u), λ(v))](u, v, ν (v)). Let m be a model over language of
SymPath(P, p, ν ) such that m restricted to {u, v } ∪ ν (v) is i(d). Since this property of m holds for all control edges (u, v) ∈ E then
m ⊢ SymPath(P, p, ν ) by the definition of SymPath.

33

Now, let a model m of SymPath(P, p, ν ) be given. The process above can almost be reversed to obtain models m D and i(d ) for
each d ∈ Nodes[D], but for each clause in G with constraint ψ , care must be taken surrounding the extra condition which ψ entails,
described in §5.3.1. Because the encoding of loads and stores requires that every live object be held by some local state variable, if an
object is not passed from R, resp. to R, this object is guaranteed to not have any of its fields modified on the control paths between
any of the ⇝+R pairs, resp. ⇝−R pairs. Therefore, ψ does not overconstrain i(d ), and we have a model (D, m D , i) of G inducing p and
(N , E Data ).

□

Lemma 3. P is simulated by SynGrammar (P, F).
Proof. SynGrammar begins by creating a CHC system C = SynSkeleton(P, F ). By the specification of SynSkeleton, C is
complete for P; i.e., every path p ∈ Paths[P] is the control graph modeled by some derivation of C.
SynGrammar then constructs the run grammar G corresponding to C. By Lemma 5, for every path p ∈ Paths[P], there is a
derivation D of G iff there is a model of SymPath(P, p, ν ) for some neighborhood ν . By Lemma 4 and Lemma 2, there is a model of D
iff there is a run of p. Therefore, G simulates every path p ∈ Paths[P], and thus simulates P.

□

Theorem 1. If Lttp(P) = True, then P is safe, and if Lttp(P) = False, then P is not safe.
Proof. Lttp returns True only if SolveCHC finds a solution to G = SynGrammar(P, F ), which proves that G is empty. By
Lemma 3, G simulates P, and with Lemma 1, this proves P is safe.
Lttp returns False only if a derivation and model (D, m, i) of G is found for which IsFeas(P, p) = True, where p is the control
graph induced by (D, m, i). (And p is path of P because G is a path grammar of P.) By Lemma 2, p is feasible run of P, witnessing that
P is not safe.

□

34

