2LS for Program Analysis

Daniel Kroening,
Viktor Malík,
Peter Schrammel and
Tomáš Vojnar

Daniel Kroening University of Oxford, United Kingdom and Diffblue Ltd,
United Kingdom<EMAIL_ADDRESS>Viktor Malík Faculty of Information Technology, Brno University of
Technology, Czech Republic and IT4Innovations Centre of Excellence, Czech Republic,
<EMAIL_ADDRESS>Peter Schrammel University of Sussex, Brighton, United Kingdom and
Diffblue Ltd, United Kingdom<EMAIL_ADDRESS>Tomáš Vojnar Faculty of Information Technology, Brno
University of Technology, Czech Republic and IT4Innovations Centre of
Excellence, Czech Republic<EMAIL_ADDRESS>
§ INTRODUCTION

2LS ("tools") is a verification tool for C programs,
built upon the CPROVER framework. It allows one to verify user-specified
assertions, memory safety properties (e.g. buffer overflows),
numerical overflows, division by zero, memory leaks, and
termination properties.

The analysis is performed by translating the
verification task into a second-order logic formula over bitvector,
array, and floating-point arithmetic theories. The formula is solved
by a modular combination of algorithms involving unfolding and
template-based invariant synthesis with the help of incremental
SAT solving.

Advantages of 2LS include its very fast incremental bounded model
checking algorithm and its flexible framework for experimenting with
novel analysis and abstraction ideas for invariant inference.
Drawbacks are its lack of support for certain program features
(e.g. multi-threading).

Table <ref> gives an overview of 2LS' features.

The remainder of the chapter is structured as follows:

* Section <ref> gives a high-level overview of the motivations and the theory behind 2LS' verification approach.

* Section <ref> provides practical information on 2LS and
how to use it for selected kinds of verification tasks, such as
proving functional properties and checking for memory safety, termination
and overflows.

* Sections <ref>–<ref> describe the
underlying theoretical concepts behind 2LS.

* Section <ref> provides details on the 2LS software
project and its architecture.

* Section <ref> reports data on experimental comparisons in the Software Verification Competition, in which 2LS has been participating since 2016.

Features of 2LS.

Languages      C, GOTO

Properties     , memory safety, overflow, division-by-zero,

Environments      Linux

Technologies used      symbolic execution, bounded model checking

abstract interpretation

template-based predicate synthesis

ranking functions, recurrent sets

SAT and SMT solving

Other features     multiple input files, compilation and linking of entire projects into GOTO via

Current strengths      memory safety, floating point, loops

Current weaknesses     recursion, multi-threading

§ VERIFICATION APPROACH

The software verification literature contains a wide range of
techniques which can be used to prove or disprove properties about
programs, each with their own strengths and weaknesses.  This presents
quite a challenge for non-expert users.

Often the choice of which tools to use and where to expend effort depends on
whether the properties to be verified are true or not—which is exactly what
they want to find out.

Hence, to build a robust and usable software verification system, it is
necessary to combine a variety of techniques.

One option would be to run a series of independent tools, in parallel
(as a portfolio, for example) or in some sequential order.  However,
this limits the information that can be exchanged between the

Another option would be to use monolithic algorithms such as
CEGAR [9], IMPACT [27], or IC3/PDR [3, 18]
which combine some of the ideas of simpler systems. These are
difficult to implement well as their components interact in complex
and subtle ways.  Also, they require advanced solver features such as
interpolant generation that are not widely available for all theories
(bit-vectors, arrays, floating-point, etc.). 2LS takes a different approach to
the problem as explained below.

§.§ $k$-induction and $k$-invariants ()

2LS strives to build a verifier as a compound
with simple components and well-understood interaction.

These include:

Bounded Model CheckingGiven sufficient time and resource, BMC
will give counterexamples for all false safety properties,
which are often of significant value for understanding the fault.
However, only a small proportion of true properties can
be proven by BMC.

$\mathbf{k}$-InductionGeneralising Hoare logic's ideas of loop
invariants, $k$-induction can prove true safety properties, and, in some
cases, provide counterexamples to false ones.
However, it requires inductive invariants, which can be expensive (in
terms of user time, expertise, and maintenance).

Abstract InterpretationThe use of over-approximations makes
it easy to compute invariants which allow many true
propositions to be proven.  However false properties and
true-but-not-provable properties may be indistinguishable.
Tools may have limited support for a more complete analysis.

2LS's algorithm [4] draws together a range of
well-known techniques and combines them in a novel way so that they
strengthen and reinforce each other.  The $k$-induction
technique [36] uses syntactically restricted or simple
invariants (such as those generated by abstract interpretation) to
prove safety.  Bounded model checking [2] allows us to test
$k$-induction failures to see if they are real counterexamples or, if
not, to build up a set of assumptions about system behaviour.
Template-based abstract interpretation is used for invariant
inference [32, 31, 16] with unrolling producing
progressively stronger invariants, allowing the techniques to
strengthen each other.

unifies these techniques in a simple and elegant algorithm for integrated
invariant inference and counterexample generation.

The main loop of $\kiki$ is based
on incremental unwinding of the transition relation.

In the $k$-th iteration, the transition relation is unwound
up to depth $k$ and a $k$-inductive invariant is inferred. The
invariant is then used to strengthen the program's safety property in
order to find a proof for the program's safety. In case that safety
cannot be proved, the algorithm checks whether the current unwinding is
sufficient to generate a counterexample. If this is not the case, the
unwinding $k$ is incremented and another iteration starts.
The $\kiki$ algorithm is explained in more detail in Section

Internally, 2LS reduces program analysis problems expressed in second
order logic such as invariant or ranking function inference to
synthesis problems over templates. Hence, it reduces (an existential
fragment of) 2nd order Logic Solving to quantifier elimination in
first order logic. Loop unwinding as used by bounded model checking
and $k$-induction are considered as refinements of the original
program abstraction.

That way, 2LS provides an efficient implementation of based on
incremental loop unwinding, template-based predicate synthesis, and,
ultimately, incremental SAT solving.

These concepts, along with other important underlying concepts of 2LS
are explained in more detail throughout Sections <ref>,
<ref>, and <ref>.

§ USE CASES

Before explaining the theoretical concepts behind 2LS, we give an overview of
2LS verification capabilities in the form of a tutorial.

2LS has a broad set of functionalities that allows the user
to solve a variety of verification problems.

We will use example programs, which can be found at <https://github.com/diffblue/2ls/tree/master/regression/book-examples>.

§.§ Proving Functional Properties

Functional properties can be specified in C programs with the help
of assertions, as provided by .

In order to state preconditions, the CPROVER framework provides
the  function.
[In order to keep the code compilable, this function can be surrounded
by , which is defined when running

As a first example, let us consider the function in
Figure <ref>, which extracts the authority part of
a URI given as a character string  into the buffer

We would like to ensure that we do not copy beyond the length of the URI,
which is expressed by the assertion on line 9.

void copy_authority(
char *uri, int uri_length, int authority_start, char *authority)
__CPROVER_assume(0 < uri_length);
__CPROVER_assume(0 < authority_start        authority_start < uri_length);
int cp = authority_start;
while (cp != uri_length - 1)
if (uri[cp] == '/')
assert(cp < uri_length);
authority[cp - authority_start] = uri[cp];

: numerical computations in a loop.

extern int __VERIFIER_nondet_int();

#include <stdlib.h>
#include <limits.h>

#define APPEND(l,i) i->next=l; l=i;

typedef struct node
struct node *next;
int val;

int main()
Node *l = NULL;
int min = INT_MAX;

while (__VERIFIER_nondet_int())
Node *p = malloc(sizeof(*p));
p->val = __VERIFIER_nondet_int();
APPEND(l, p)

if (min > p->val)
min = p->val;

for (Node *i = l; i != NULL; i = i->next)
assert(i->val >= min);

: data stored in a dynamically allocated data structure.

2LS provides various algorithms for verifying this property. For example:

2LS performs a 1-induction check using the invariant $\true$.
This is not sufficient to prove the property.
Hence, it returns .

2LS performs a 1-induction check using the interval invariants.
This is still not sufficient. We get the result .

Using the stronger zones abstract domain, we are able to prove the property.
2LS outputs .

The even stronger octagons abstract domain allows us to prove the property,
too. 2LS returns .

2LS performs $k$-induction. This is sufficient to prove the property, even
though we do not infer additional invariants (the  option).
2LS reports .

The example above dealt with numerical data. Let us now have a look at the
program in Figure <ref>. This program allocates a
singly-linked list of arbitrary length whose elements hold some integer value.

[The  function is declared
but does not have a definition. 2LS assumes that functions without
definition return a non-deterministic value.]

It then computes the imum value held by the list elements
and checks whether the minimum has been computed correctly, i.e.,
it must be smaller than or equal to all values in the list.

2LS can prove this thanks to combined reasoning about the shape of
unbounded data structures and their contents at the same time.

will return  for the property on line 26[The
options employ a combination of shape and
numerical domains.].
This means that the assertion is not violated by any list of any size.

§.§ Finding Memory Safety Bugs

Another class of properties that can be verified using 2LS is that of memory
safety properties. These include, e.g., array accesses within bounds, pointer
dereference safety, free safety, or absence of memory leaks. 2LS performs
verification of these properties by instrumenting the program with custom
assertions. The complete list of available instrumentations can be seen by
running 2LS with the  option.

We demonstrate verification of memory safety properties on two examples. First,
let us consider the program in Figure <ref> which
transforms a two-dimensional array  into a single-dimensional
array . We let the matrix dimensions to be random, but we add a
precondition on line 7 assuring that the number of matrix elements fits the
destination array.

#define SIZE 1000

int main()
int **matrix;
unsigned m = __VERIFIER_nondet_int();
unsigned n = __VERIFIER_nondet_int();
__CPROVER_assume(m <= SIZE        n <= SIZE        m * n <= SIZE);

int array[SIZE];
for (int row = 0; row < m; ++row)
for (int col = 0; col < n; ++col)
int index = row * m + col;
array[index] = matrix[row][col];

return 0;

: array bounds safety.

Running the verification with

will return  with an additional information about the
particular generated assertion that failed:

This information says that  may be larger than the
array's upper bound (). Furthermore, 2LS is able to provide a
concrete counterexample in case it found a property violation. We may get this
by re-running 2LS with an additional  option. An important
part of the obtained trace is shown in Figure <ref>.

Counterexample for array bound safety violation for program in
Figure <ref>.

Using the counterexample, we discover an error on line 12, which should
[firstnumber=12, basicstyle=,
int index = row * n + col;

Running the verification again after correcting the error returns ,
which means that no more out-of-bounds array accesses are present in the

For the second example of memory safety verification, we consider the program
containing a dynamic memory allocation shown in
Figure <ref>. The program allocates two memory objects
pointed by pointers  and  and linked together (the value of
the object pointed by  equals to  which points to a
random integer). Afterwards, both allocated objects are freed.  However, the
freeing order is incorrect since  is freed first and an attempt to
free the pointed object will likely fail due to an invalid dereference of a
dangling pointer. 2LS can be used to verify absence of pointer dereference and
of memory free errors by running

As expected, running this command on the shown program returns
with an additional information about the error:

int main()
int *a = malloc(sizeof(int));
*a = __VERIFIER_nondet_int();

int **b = malloc(sizeof(int *));
*b = a;

: free safety verification.

§.§ Termination and Nontermination

2LS can prove whether a program is terminating or
whether it may not terminate under certain input conditions.

void bubble_sort(int *array, int size)

__CPROVER_assume(size >= 0);
int c, d, swap;

for (c = 0; c < size - 1; c++)

for (d = 0; d < size - c - 1; d++)

if (array[d] > array[d + 1])

swap       = array[d];
array[d]   = array[d + 1];
array[d + 1] = swap;

: proving termination.

For example, Figure <ref> shows
an implementation of the bubble sort algorithm.

We can check whether it terminates by running the following:

We get an output of the following sort:

2LS computes a termination argument in the form of a ranking function.
The termination argument in the output above is heavily simplified to
make it fit on this page. The actual termination argument output by 2LS
has more elaborate guard constraints and casts to enable correct bitvector
arithmetic without overflows.

An inspection of the termination argument says that  is a
ranking function for the outer loop and  is a ranking
function for the inner loop, which proves termination of the

long sasum(long *sx, int n, int incx)

int nincx = n * incx;
long stemp = 0l;
int i;
for (i = 0; incx < 0 ? i >= nincx : i <= nincx; i += incx)

stemp += sx[i-1];

return stemp;

(cf. <http://www.netlib.org/clapack/cblas/sasum.c).>

2LS can also check for non-termination. It will do this by finding
lasso-shaped executions. Figure <ref> shows
an array summation algorithm from a linear algebra package.

gives the output shown in Figure <ref>.

Inspecting the counterexample trace, we see that variable
has the recurring value  on line 6, which implies
non-termination of the loop because the loop condition can never
become false. We can even see an example of input conditions
under which this happens: .

Output for the non-termination example.

In practice, one can run  and
in parallel and wait for the first to
report a conclusive result.

§.§ Overflows

Another property that can be verified using 2LS is safety from integer
overflows (and underflows). Similarly to memory safety verification, it is done
by instrumenting the analysed program with custom assertions.

As an illustration, we use the program in Figure <ref>. In
the program, the precondition  on line 3
is necessary to avoid signed arithmetic underflows in computing , which would be an undefined behaviour in the C standards supported by 2LS.
We can verify this by running 2LS to check for overflows:

Without the precondition, we would get:

which confirms the necessity of the precondition.

§ INTERNAL PROGRAM REPRESENTATION

Being built upon the CPROVER
infrastructure [8], 2LS uses GOTO
programs as an intermediate representation.  In this language, any
non-linear control flow, such as if or switch-statements, loops, or
jumps, is translated to equivalent guarded goto statements.
These statements are branch instructions that include
(optional) conditions.  CBMC generates one GOTO program per C function
found in the parse tree.  Furthermore, it adds a new main function
that first calls an initialisation function for global variables and
then calls the original program entry function.

Similarly to CBMC, 2LS performs a light-weight static analysis to resolve
function pointers to a case split over all candidate functions, resulting in
a static call graph.  Furthermore, assertions guarding against invalid
pointer operations or memory leaks are inserted. In addition, 2LS uses local
constant propagation and expression simplification to increase efficiency.

After running the mentioned transformations, 2LS performs a static analysis to
derive data flow equations for each function of the GOTO program.  The result
is a static single assignment (SSA) form in which loops have been cut
at the back edges to the loop head.  The effect of these cuts is havocking of
the variables modified in the loop at the loop head.  This SSA is hence an
over-approximation of the GOTO program. Subsequently, 2LS refines this
over-approximation by computing invariants.

Since this SSA representation is crucial for the verification approach
of 2LS, we give its detailed description in
Section <ref>. Prior to that, we introduce our memory model
that is used to represent dynamically allocated objects in our SSA
form (Section <ref>). At last, we give
an insight into our loop unwinding approach, which is an imporant step
of the $\kiki$ algorithm, in Section <ref>.

§.§ Memory Model

We now describe a memory model that we use to represent all program
memory [22]. Our model is object-based, and we distinguish objects
allocated statically (i.e., variables on the stack and global variables)
and dynamically (i.e., on the heap).

§.§.§ Static memory objects

In our approach, we work with non-recursive programs with all functions
inlined. Therefore, we do not need to consider the stack and the set $\var$ of
static memory objects corresponds to the set of all program variables. Each
variable is uniquely identified by its name.

For convenience, we define subsets of $\var$ that correspond to sets of
variables of a chosen type:

* $\nvar$ is the set of all variables of a numeric type (integer or
floating point).

* $\pvar$ is the set of all variables of a pointer type.

* $\svar$ is the set of all variables of a structure type. Each structure
type defines a set of named fields, each of them having its own
type. We use $\fld$ to denote the set of all fields used in the analysed
program.  Similarly to the variables, we let $\nfld, \pfld \subseteq \fld$
be the sets of all fields of numerical and pointer types, respectively. In
order to express access to individual fields of a structure-typed variable,
we use the “dot” notation as is common in C.

We assume $\nvar$, $\pvar$, and $\svar$ are pairwise disjoint.

§.§.§ Dynamic memory objects

To represent dynamic memory objects (i.e., those allocated using
or some of its variants), we use abstract dynamic
objects. An abstract dynamic object represents a set of concrete dynamic
objects allocated by the same  call. We refer to a
call at a program location $i$ as to an allocation site

Generally, a single abstract dynamic object is not sufficient to represent all
concrete objects allocated by a single  call. This is due to the
fact that the analysed program may use several concrete objects allocated at
the same allocation site at the same time. If such objects are, e.g., compared,
our memory model must allow us to distinguish them. This can be done either by
concretisation on demand (as is common in many memory models) or by
pre-materialisation of a sufficient number of objects at the beginning of the
analysis. Since our approach uses a single formula to represent the analysed
program and leverages on small incremental changes of the formula during the
analysis, we use the latter approach.

Therefore, we use the set $\dynobjset{i} = \{\dynobj{i}{k} \mid 1 \leq k \leq
n_i\}$ of abstract objects to represent all concrete objects allocated at the
allocation site $i$. The number $n_i$ of necessary objects is determined for
each allocation site using an approach described later in this section. The set
of all dynamic objects of the analysed program is then defined as $\dobj =
\cup_i \dynobjset{i}$. Together with the set of all static objects, we define
$\obj = \var \cup \dobj$ to be the set of all memory objects of our program
abstraction. We require $\var \cap \dobj = \emptyset$ and $\dynobjset{i} \cap
\dynobjset{j} = \emptyset$ for $i \neq j$.

Similarly to static objects, we denote $\ndobj$, $\pdobj$, and $\sdobj$ the
sets of dynamic objects of a numerical, pointer, and structure type,
respectively. Fields of structure-typed dynamic objects, i.e., elements of the
set $\sdobj \times \fld$, represent abstractions of the appropriate field of
all represented concrete objects. Using the above sets, we may define the set
$\num$ of all numerical objects in the program as:

\begin{equation}
\num = \nvar \cup \ndobj \cup ((\svar \cup \sdobj) \times \nfld).
\end{equation}

Analogically, we define the set $\ptr$ of all pointers as:

\begin{equation}\label{eq:pointers}
\ptr = \pvar \cup \pdobj \cup ((\svar \cup \sdobj) \times \pfld).
\end{equation}

Pointers can be assigned addresses of objects. Since we do not support pointer
arithmetic, only symbolic addresses and a special address $\nullptr$ are
considered. We use the operator & to get the address of both static and
dynamic objects. For abstract dynamic objects, the symbolic address is an
abstraction of symbolic addresses of all represented concrete objects. We
define the set $\addr$ of all addresses in the program as:

\begin{equation}
\addr = \{\&o \mid o \in \obj\} \cup \{\nullptr\}.
\end{equation}

§.§.§ Dynamic Object Pre-Materialisation

Above, we mentioned that, for each allocation site $i$, we represent (a
potentially infinite number of) all objects allocated at $i$ by a finite number
$n_i$ of abstract dynamic objects. In order for this abstraction to be sound,
it is sufficient that this number is equal to the number of distinct concrete
objects, allocated at $i$, that may be simultaneously pointed to at any
location of the analysed program.

In order to compute this number, we first perform a standard static
may-alias analysis. This analysis determines, for each program location
$j$, the set $P_i^j$ of all pointer expressions used in the program,
that may point to some object allocated at $i$. Here, pointer expressions may
be one of the following:

* Pointer variables.

* Dereferences of pointers to pointers. These correspond to pointer-typed
dynamic objects.

* Pointer fields of structure-typed variables.

* Dereferences of pointers to structures followed by an access to a
pointer-typed field. These correspond to pointer-typed fields of dynamic
objects.  Here, we use the C notation based on an arrow (e.g.,
$p\!\!\rightarrow\!\!n$ to express a dereference of $p$ followed by an
access to the
field $n$ of the pointed object).

For simplicity, we assume that all chained dereferences of forms **$p$ or
$p\!\!\rightarrow\!\!f_1\!\!\rightarrow\!\!f_2$ are split into multiple
dereferences using an
intermediate pointer variable which is added to $\pvar$.

Next, we compute the must alias relation $\sim_j$ over the set of all pointer
expressions. For each pair of pointer expressions $p$ and $q$ and for each
program location $j$, $p \sim_j q$ iff $p$ and $q$ must point to the same
concrete object (i.e., they must alias) at $j$.

Finally, we partition each computed $P^j_i$ into equivalence classes by
$\sim_j$, and the number $n_i$ is given by the maximal number of such classes
for any $j$.

§.§ The Static Single Assignment Form

Program verification in 2LS is based on generating program abstractions using a
solver. In order to simplify generation of a formula representing the program
semantics, 2LS uses the static single assignment form (SSA) to represent
programs. SSA is a standard program representation used in bounded model
checking or symbolic execution tools. We use common concepts of
SSA—introducing a fresh copy (version) $x_i$ of each variable $x$ at program
location $i$ in case $x$ is assigned to at $i$, using the last version of $x$
whenever $x$ is read, and introducing a phi variable $\ssaxphi{i}$ at a
program join point $i$ in case different versions of $x$ come from the joined
program branches. For an acyclic program, SSA is a formula that represents
exactly the post condition of running the code.

We extend the traditional SSA by three new concepts: (1) over-approximation of
loops in order to make the SSA acyclic [4], (2) a special encoding of
the control-flow [4], and (3) a special representation of
memory-manipulating operations that comply with our memory model introduced
in Section <ref> [22]. In the rest of this section, we
describe these extensions.

§.§.§ Over-Approximation of Loops

In order to be able to use a solver for reasoning about program abstractions,
we extend the SSA by over-approximating the effect of loops. As was said
above, the value of a variable $x$ is represented at the loop head by a phi
variable $\ssaxphi{i}$ joining the value of $x$ from before the loop and from
the end of the loop body (here, we assume that all paths in the loop join
before its end, and the same holds for the paths before the loop). However,
instead of using the version of $x$ from the loop end, it is replaced by a
free loop-back variable $\ssaxlb{}$. This way, the SSA remains acyclic,
and, since the value of $\ssaxlb{}$ is initially unconstrained, the effect of
the loop is over-approximated. To improve precision, the value of $\ssaxlb{}$
can be later constrained using a loop invariant that will be inferred
during the analysis. A loop invariant is a property that holds at the end of
the loop body, after any iteration and can be therefore assumed to hold on the
loop-back variable.

For a better illustration, we give an example of this SSA extension.
Figure <ref> shows a simple loop in C and its corresponding SSA.
Instead of using $\ssax{5}$ in the phi variable, a fresh variable $\ssaxlb{6}$
is introduced. Moreover, the join in the phi node is driven by a free Boolean
variable $\ssagls{6}$ (a so-called loop-select guard) modelling a
non-deterministic choice between $\ssaxlb{6}$ and $\ssax{0}$.

unsigned x = 0;

while (x < 10)

A loop in C.

[] (i) at (0,0) before the loop;
[] (i2) at (0,-0.5) $\ssax{0} = 0$;
[] (1) at (-1.9, 0.01) 1:;
[] (h) at (0,-2) loop head;
[] (3) at (-1.9, -1.98) 3:;
[] (h2) at (0,-2.5) $\ssaxphi{3} = \ssagls{6} \;?\; \ssaxlb{6} \;:\; \ssax{0}$;
[] (b) at (0,-3.5) loop body;
[] (4) at (-1.9, -3.49) 4:;
[] (b2) at (0,-4) $\ssax{5} = \ssaxphi{3} + 1$;
[] (5) at (-1.9, -3.99) 5:;
[] (e) at (0,-5) end of the loop body;
[] (6) at (-1.9, -4.99) 6:;
[] (a) at (0,-6) after the loop;

[->] (i2) edge (h);
[->] (h2) edge (b);
[->] (b2) edge (e);
[->] (h2.south west) edge[bend right=60, looseness=2] (a.west);
[->] (e.east) edge[bend right=80, looseness=2] node[right]$\ssaxlb{6}$ (h.east);

Encoding of the loop in the SSA form.

Conversion of loops in the SSA form used in 2LS.

§.§.§ Encoding the Control-Flow

In 2LS, the program is represented by a single monolithic formula. It is
therefore needed that the formula encodes control-flow information. This is
achieved using so-called guard variables that track the reachability
information for each program location. In particular, for each program location
$i$, we introduce a Boolean variable $\ssag{i}$ whose value encodes whether
$i$ is reachable. For example, in Figure <ref>, a guard
$\ssag{5}$ encoding reachability of the loop body would have the value:

\begin{equation}
\ssag{5} = \ssaxphi{3} < 10.
\end{equation}

§.§.§ Representation of Memory-Manipulating

§.§.§ Dynamic Memory Allocation

As said in Section <ref>, all concrete objects allocated by a
single  call at a program location $i$ are abstracted by a set
of abstract dynamic objects $\dynobjset{i}$. In the SSA form, we represent such
a call by a non-deterministic choice among objects from $\dynobjset{i}$. A
program assignment  is therefore transformed into the

\begin{equation}
\ssa{p}{i} = \ssagosij{i}{1} \,?\, \&\dynobj{i}{1} :
(\ssagosij{i}{2} \,?\, \&\dynobj{i}{2} : (\ldots (\ssagosij{i}{n_i-1}
\,?\, \&\dynobj{i}{n_i-1} : \&\dynobj{i}{n_i})))
\end{equation}

where $\ssagosij{i}{j}$, $1 \leq j < n_i$, are free Boolean variables, so-called
object-select guards.

§.§.§ Reading through Dereferenced Pointers

We now describe encoding of a pointer dereference appearing on the right-hand
side of an assignment or in a condition (i.e., in an R-expression).  Prior to
generating the SSA, we perform a static may-points-to analysis which
over-approximates—for each program location $i$ and for each pointer $p \in
\ptr$—the set of all objects from $\obj$ that $p$ may point to at $i$. A
dereference of $p$ at $i$ is then represented by a choice among the pointed

Moreover, to simplify the representation and to improve precision (for reasons
explained below), we also introduce so-called dereference variables.

Let $*p$ be an R-expression that appears at a program location $i$ and let us
assume that $p$ may point to a set of objects $O \subseteq \obj$. We replace
$*p$ by a fresh variable $\drfvar{p}{i}$, and we define its value as follows:

\begin{equation}\label{eq:mem_read}
\begin{split}
&\bigwedge_{o \in O} \ssa{p}{j} = \&o \Longrightarrow \drfvar{p}{i} = \ssa{o}{k}
\;\wedge\\
&\left(\bigwedge_{o \in O} \ssa{p}{j} \neq \&o\right) \Longrightarrow
\drfvar{p}{i} = o_\perp
\end{split}
\end{equation}

where $\ssa{p}{j}$ and $\ssa{o}{k}$ are the relevant versions of the variables $p$
and $o$, respectively, at the program location $i$, and $o_\perp$ is a special
“unknown object” representing the result of a dereference of an unknown or
invalid ($\nullptr$) pointer.

Informally, (<ref>) expresses the fact that $\drfvar{p}{i}$
equals the value of $o$ at $i$ in case that $p$ points to $o$ at $i$, and
it equals the value of the unknown object otherwise.

§.§.§ Writing through Dereferenced Pointers

Similarly to the operation of reading, we introduce an SSA encoding for the
operation of writing into memory using a pointer dereference. Again, we leverage
on a may-points-to analysis described above, and we introduce special
dereference variables.  Let us have an assignment $*p = v$ at program
location $i$ and let us assume that $p$ may point to a set of objects $O
\subseteq \obj$ at the entry to $i$.  This assignment is replaced by an

\begin{equation}
\drfvar{p}{i} = \ssa{v}{l}.
\end{equation}

where $\ssa{v}{l}$ is the valid version of $v$ at $i$. The dereference variable
$\drfvar{p}{i}$ is then used to update the value of the referenced object. This
is done using the formula:

\begin{equation}
\bigwedge_{o \in O} \ssa{o}{i} =
(\ssa{p}{j} = \&o) \,?\, \drfvar{p}{i} : \ssa{o}{k}
\end{equation}

where $\ssa{p}{j}$, $\ssa{o}{k}$ are relevant versions of the variables $p$ and
$o$, respectively, at program location $i$.

In other words, this formula expresses the fact that an object $o$ is assigned
the value of $v$ in the case when $p$ points to $o$, and it keeps its original
value otherwise. As mentioned above, usage of dereference variables may improve
precision of the representation. This happens especially when we write into an
abstract object through some pointer and afterwards read through the same
pointer without changing its value nor the value of the pointed object in
between. In such cases, we may reuse the same dereference variable which ensures
that we get the same value that was written, which may not happen otherwise
since we read from an abstract object representing a number of concrete objects.

§.§ Structural Transformations

The algorithm uses loop unwinding to refine the
control flow structure of the program.

There are several possible strategies of how to
perform this unwinding.
We have experimented in  [35]
with an unwinding strategy that follows the control flow
and unwinds loops one by one and performs property checking
after each unwinding.

With such a strategy, each loop is incrementally unwound until all
paths exit the loop or until a maximum depth $k$ is reached. We can
detect that a loop is fully unwound at unwinding $j<k$ if every state
reached at unwinding $j$ does not satisfy the loop condition.  After
a loop has been unwound, continues to the next loop. This
procedure is repeated until all loops have been unwound or a bug has
been found.  Recursive function calls are treated similarly.

Consider the control flow graph (CFG) in Fig. <ref>(a).  The
unwinding strategy is illustrated for this CFG in
Fig. <ref>(b).  The program has three loops with loop
heads 1, 2, and 6 (2 is nested inside 1).  The symbolic execution that
generates the incremental BMC formula $\Phi(k)$ (see
Section <ref>) traverses the CFG and stops each time when it
encounters an edge in the CFG that returns to a loop head (a so-called
back-edge).  Fig. <ref>(b) shows three snapshots of
the partially unwound CFG that correspond to the parts of the program
considered by instances of the incremental BMC formula $\Phi(k)$ for
$k=1,2,m$.  We write $\Phi(1)$ for the formula up to the first back-edge
encountered that returns to the loop head of the inner loop (2).  Formula
$\Phi(2)$ extends $\Phi(1)$ by one further unwinding of the inner loop.
Assume that $m$ is the maximum number of unwindings of the inner loop, then
$\Phi(m)$ shows the extension of the formula to the case where the inner
loop has been unwound up to this maximum number within the first iteration
of the outer loop (with loop head 1).  Formula $\Phi(m+1)$ will then extend
$\Phi(m)$ by a first unwinding of the inner loop (up to program location 4)
for the second iteration of the outer loop.  This process continues until a
failed assertion or the end of the program (8) is reached.

We realised that this approach is not very efficient. Hence,
we implement a different approach in 2LS [34, 4].

2LS unwinds all loops $k$ times and incrementally adds the
$(k+1)\text{th}$ for all loops instead of unwinding only the
first loop encountered until it has been fully unwound.

We illustrate this unwinding strategy in Fig. <ref>(c), which
shows the first two partial unwindings of the CFG in
Fig. <ref>(a) that correspond to $\Phi(1)$ and $\Phi(2)$,
respectively.  Formula $\Phi(1)$ consists of one unwinding (up to, but not
including the back-edge) for the loops 1, 2, and 6.  Formula $\Phi(2)$ then
adds another unwinding to each loop.  Note that we have two times two
unwindings of the inner loop (with loop head 2) now, two for each unwinding
of the outer loop (loop head 1).

Structurally, this unwinding strategy is the same as the one that we
use in non-incremental when calling it with fixed values for $k$.

2LS performs loop unwinding on the SSA form augmented with some meta-information
on the loop structure and hierarchy.

The unwinding that we perform is incremental, in the sense that we incrementally
extend the SSA when increasing $k$ to $k+1$.

The problematic part is the merging of loop exits (nodes 5, 6, and 8 in
Fig. <ref>(c)).

We have to account for the case of “value is merged from an unwinding that has
not been added yet”, which makes the construction of the formula non-monotonic.

Indeed, one has to effectively remove the disjunction describing each
such merge, which represents one conjunct in the SSA form, and replace it by a
larger disjunction reflecting the addition of a new incoming branch of the
concerned merge obtained by an additional unwinding.

Removing parts of the formula, however, is not supported by SAT solvers.

Fortunately, this problem can be solved with the help of solving under
assumptions as we will explain in Section <ref>.

This is an essential ingredient for performance as it enables the use of a
single SAT solver instance to run incremental BMC and ultimately the
entire algorithm.

A disadvantage of the approach is that many optimisations that can be
typically done during symbolic execution in order to simplify the
formula, such as constant propagation, can only be done locally, if at

An example of a program with three loops.[0.8]

[draw,circle](n0) at (0,9.5) 0;
[draw,circle](n1) at (0,8.5) 1;
(p1l) at (-1,8.5);
(p1r) at (1,8.5);
[draw,circle](n2) at (0,7.5) 2;
(p2l) at (-0.5,7.5);
(p2r) at (0.5,7.5);
[draw,circle](n3) at (0,6.5) 3;
[draw,circle](n4) at (0,5.5) 4;
(p4r) at (0.5,5.5);
(p5l) at (-0.5,4.75);
(p5) at (0,4.75);
(p5r) at (1,4);
[draw,circle](n5) at (0,4) 5;
(p6l) at (-1,3.25);
(p6) at (0,3.25);
[draw,circle](n6) at (0,2.5) 6;
(p6r) at (1,2.5);
[draw,circle](n7) at (0,1.5) 7;
(p7r) at (1,1.5);
(p7l) at (-1,2.5);
(p8l) at (-1,0.75);
(p8) at (0,0.75);
[draw,circle](n8) at (0,0) 8;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);
[->] (n6) – (n7);
[->] (n1) – (p1l) – (p6l) –(p6) –(n6);
[->] (n4) – (p4r) – (p2r) – (n2);
[->] (n2) – (p2l) – (p5l) – (p5) – (n5);
[->] (n5) – (p5r) – (p1r) – (n1);
[->] (n6) – (p7l) – (p8l) – (p8) – (n8);
[->] (n7) – (p7r) – (p6r) – (n6);

Incremental unwinding strategy of

(b0) at (0,10.5) $\overbrace{\hspace*{2em}}^{\Phi(1)}$;
(b1) at (1.5,10.5) $\overbrace{\hspace*{4em}}^{\Phi(2)}$;
(b2) at (4.25,10.5) $\overbrace{\hspace*{8em}}^{\Phi(m)}$;
(b3) at (6.5,10.5) …;
(n00) at (6.5,9.5) …;
[draw,circle](n0) at (0,9.5) 0;
[draw,circle](n1) at (0,8.5) 1;
[draw,circle](n2) at (0,7.5) 2;
[draw,circle](n3) at (0,6.5) 3;
[draw,circle](n4) at (0,5.5) 4;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);

[draw,circle](n0) at (1,9.5) 0;
[draw,circle](n1) at (1,8.5) 1;
[draw,circle](n2) at (1,7.5) 2;
[draw,circle](n3) at (1,6.5) 3;
[draw,circle](n4) at (1,5.5) 4;
(p4r) at (1.5,5.5);
(p22l) at (1.5,8);
(p22) at (2,8);
[draw,circle](n22) at (2,7.5) 2;
[draw,circle](n33) at (2,6.5) 3;
[draw,circle](n44) at (2,5.5) 4;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);
[->] (n4) – (p4r) – (p22l) – (p22) – (n22);
[->] (n22) – (n33);
[->] (n33) – (n44);

[draw,circle](n0) at (3,9.5) 0;
[draw,circle](n1) at (3,8.5) 1;
[draw,circle](n2) at (3,7.5) 2;
(p2l) at (2.6,7.5);
[draw,circle](n3) at (3,6.5) 3;
[draw,circle](n4) at (3,5.5) 4;
(p4r) at (3.4,5.5);
(p5l) at (2.6,4.75);
(p22r) at (3.4,8);
(p22) at (4,8);
(p22l) at (3.6,7.5);
[draw,circle](n22) at (4,7.5) 2;
[draw,circle](n33) at (4,6.5) 3;
[draw,circle](n44) at (4,5.5) 4;
(p44r) at (4.4,5.5);
(p55l) at (3.6,4.75);
(p222r) at (4.4,8);
(p222) at (5.5,8);
(p222l) at (5.1,7.5);
[draw,circle](n222) at (5.5,7.5) 2;
(p555l) at (5.1,4.75);
(p555r) at (4.4,4.75);
(p555) at (5.5,4.75);
[draw,circle](n555) at (5.5,4) 5;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);
[->] (n4) – (p4r) – (p22r) – (p22) – (n22);
[->] (n22) – (n33);
[->] (n33) – (n44);
(n44) – (p44r) – (p222r);
[dashed] (p222r) – (p222);
[->] (p222) – (n222);
[->] (n222) – (p222l) – (p555l) – (p555) – (n555);
(n22) – (p22l) – (p55l) – (p555r);
[dashed] (p555r) – (p555l);
(n2) – (p2l) – (p5l) – (p55l);

Incremental unwinding strategy of 2LS.[0.8]
(b0) at (0,10.5) $\overbrace{\hspace*{2em}}^{\Phi(1)}$;
(b1) at (2.75,10.5) $\overbrace{\hspace*{11em}}^{\Phi(2)}$;
(b2) at (5.5,10.5) …;
(n00) at (5.5,9.5) …;
[draw,circle](n0) at (0,9.5) 0;
[draw,circle](n1) at (0,8.5) 1;
(p1l) at (-0.75,8.5);
(p1r) at (1,8.5);
[draw,circle](n2) at (0,7.5) 2;
(p2l) at (-0.5,7.5);
(p2r) at (0.5,7.5);
[draw,circle](n3) at (0,6.5) 3;
[draw,circle](n4) at (0,5.5) 4;
(p4r) at (0.5,5.5);
(p5l) at (-0.5,4.75);
(p5) at (0,4.75);
(p5r) at (1,4);
[draw,circle](n5) at (0,4) 5;
(p6l) at (-0.75,3.25);
(p6) at (0,3.25);
[draw,circle](n6) at (0,2.5) 6;
(p6r) at (1,2.5);
[draw,circle](n7) at (0,1.5) 7;
(p7r) at (1,1.5);
(p7l) at (-0.75,2.5);
(p8l) at (-0.75,0.75);
(p8) at (0,0.75);
[draw,circle](n8) at (0,0) 8;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);
[->] (n6) – (n7);
[->] (n1) – (p1l) – (p6l) –(p6) –(n6);
[->] (n2) – (p2l) – (p5l) – (p5) – (n5);
[->] (n6) – (p7l) – (p8l) – (p8) – (n8);

[draw,circle](n0) at (1.5,9.5) 0;
[draw,circle](n1) at (1.5,8.5) 1;
(p1l) at (0.75,8.5);
(p1r) at (2.5,8.5);
[draw,circle](n2) at (1.5,7.5) 2;
(p2l) at (1,7.5);
(p2r) at (2,7.5);
[draw,circle](n3) at (1.5,6.5) 3;
[draw,circle](n4) at (1.5,5.5) 4;
[draw,circle](n22) at (2.5,7.5) 2;
(p4r) at (1.9,5.5);
(p22r) at (1.9,8);
(p22) at (2.5,8);
(p22l) at (2.1,7.5);
[draw,circle](n33) at (2.5,6.5) 3;
[draw,circle](n44) at (2.5,5.5) 4;
(p5l) at (1,4.75);
(p5) at (1.5,4.75);
(p5r) at (2.1,4.75);
[draw,circle](n5) at (1.5,4) 5;
(p6l) at (0.75,3.25);
(p6) at (1.5,3.25);
[draw,circle](n6) at (1.5,2.5) 6;
[draw,circle](n7) at (1.5,1.5) 7;
[draw,circle](n66) at (2.5,2.5) 6;
(p66r) at (1.9,3);
(p66) at (2.5,3);
(p66l) at (2.1,2.5);
[draw,circle](n77) at (2.5,1.5) 7;
(p8r) at (2.1,0.75);
(p7r) at (1.9,1.5);
(p7l) at (0.75,2.5);
(p8l) at (0.75,0.75);
(p8) at (1.5,0.75);
[draw,circle](n8) at (1.5,0) 8;
[->] (n0) – (n1);
[->] (n1) – (n2);
[->] (n2) – (n3);
[->] (n3) – (n4);
[->] (n22) – (n33);
[->] (n33) – (n44);
[->] (n4) – (p4r) – (p22r) – (p22) – (n22);
(n22) – (p22l) – (p5r) – (p5);
[->] (n6) – (n7);
[->] (n66) – (n77);
[->] (n1) – (p1l) – (p6l) –(p6) –(n6);
[->] (n2) – (p2l) – (p5l) – (p5) – (n5);
[->] (n6) – (p7l) – (p8l) – (p8) – (n8);
(n66) – (p66l) – (p8r) – (p8);
[->] (n7) – (p7r) – (p66r) – (p66) – (n66);
[draw,circle](n11) at (3.5,8.5) 1;
(p11l) at (2.9,9);
(p11) at (3.5,9);
(p11r) at (3,8.5);
(p6r) at (3,3.25);
[draw,circle](n222) at (3.5,7.5) 2;
(p222l) at (3.1,7.5);
(p222r) at (4,7.5);
(p55r) at (2.9,4);
[draw,circle](n333) at (3.5,6.5) 3;
[draw,circle](n444) at (3.5,5.5) 4;
[draw,circle](n2222) at (4.5,7.5) 2;
(p444r) at (3.9,5.5);
(p2222r) at (3.9,8);
(p2222) at (4.5,8);
(p2222l) at (4.1,7.5);
[draw,circle](n3333) at (4.5,6.5) 3;
[draw,circle](n4444) at (4.5,5.5) 4;
(p555l) at (3.1,4.75);
(p555) at (3.5,4.75);
(p555r) at (4.1,4.75);
[draw,circle](n555) at (3.5,4) 5;
[->] (n11) – (n222);
[->] (n222) – (n333);
[->] (n333) – (n444);
[->] (n2222) – (n3333);
[->] (n3333) – (n4444);
[->] (n444) – (p444r) – (p2222r) – (p2222) – (n2222);
(n2222) – (p2222l) – (p555r) – (p555);
[->] (n222) – (p222l) – (p555l) – (p555) – (n555);
[->] (n5) – (p55r) – (p11l) – (p11) – (n11);
(n11) – (p11r) – (p6r) – (p6);

Incremental unwinding strategies.

§ THE $\KIKI$ ALGORITHM

As we outlined in Section <ref>, the core of 2LS is the $\kiki$
algorithm, which we present in detail in this section. The general workflow of
the algorithm is shown in Figure <ref>.

Initially, $k = 1$ and $\tdom$ is
a set of predicates that can be used as invariant with $\top \in
\tdom$ (see Section <ref> for details of how this is implemented).

After an initial test to see if any start states are
errors, $\kiki$ computes a $k$-inductive
invariant that covers the initial state and includes the assumption
that there are no errors in earlier states.

The invariant is then checked to see whether it is
sufficient to show safety.  If there are possible reachable error
states then a second check is needed to see if the error is reachable
in $k$ steps (a genuine counterexample) or whether it is a potential
artefact of a too weak invariant.  In the latter case, $k$ is incremented
so that a stronger ($k$-)invariant can be found and the algorithm loops.

Also displayed in Figure <ref> are the steps of
incremental BMC, $k$-induction and classical over-approximating abstract
interpretation, given, respectively by the red dotted, blue dashed, and
green dashed/dotted boxes and arrows.
$\kiki$ can simulate $k$-induction by having
$\tdom = \{ \top \}$ and incremental BMC by over-approximating
the first SAT check.  Classical over-approximate abstract
interpretation can be simulated by having $\tdom = \adom$ for an abstract
domain $\adom$
and terminating with the result “unknown” if the first SAT check
finds a model.

stage/.style = drop shadow, draw, fill=white, shape=rectangle
final/.style = stage
merge/.style = fill=black, shape=circle

result/.style =

ibmc/.style = red, densely dotted
kind/.style = blue, dashed
absint/.style = green, densely dashdotted

blink/.style = thick
hlink/.style = blink, -stealth, shorten >=3pt
tlink/.style = blink, shorten <=3pt
link/.style = hlink, blink, tlink

abox/.style = ultra thin, rounded corners, fill, fill opacity=0.05

answerline = 2cm,
outsideoffset = 2.75cm,
rectx = 6.5cm,
recty = 3cm
coordinate (answerline) at (0,-1*answerline)
coordinate (outsidelow) at (-1*outsideoffset, -1*answerline)
coordinate (start) at (0, 2*recty)
coordinate (init) at (0, 1.5*recty)
coordinate (outsidehigh) at (outsidelow |- init)
coordinate (initsplit) at (0, recty)
coordinate (inv) at (rectx, recty)
coordinate (invce) at (rectx, 0)
coordinate (invcesplit) at (0.5*rectx, 0)
coordinate (concretece) at (0,0)
coordinate (increment) at (0,0.6*recty)
coordinate (ce) at (answerline -| concretece)
coordinate (unknown) at (answerline -| invcesplit)
coordinate (safe) at (answerline -| invce)

step = 0.75cm
+( 0, 0.5*step) coordinate (boxtop)
+( 0,-0.5*step) coordinate (boxtoplower)
+( 0,  step) coordinate (kikistart)
+(-0.5*step,0) coordinate (ibmcstartpart)
+(-1*step,0) coordinate (ibmcstart)
+( 0.5*step,0) coordinate (kindstartpart)
+( 1*step,0) coordinate (kindstart)
coordinate (absintstart) at (kikistart -| inv)

insetwidth = 0.6cm,
insetheight = 1cm
+(0,-1) coordinate (boxbottom)
+(3,0) coordinate (boxright)
+(-3,0) coordinate (boxleft)
+(-0.5,0) coordinate (innerleft)
+(-1*insetwidth,0) coordinate (insetleft)
+( 1*insetwidth,0) coordinate (insetright)
+( 0, 1*insetheight) coordinate (insettop)
+(2.7,0) coordinate (innerright)

[abox, ibmc] (boxleft |- boxtop) – (ibmcstartpart |- boxtop) – (kindstartpart |- boxtoplower) – (boxtoplower -| innerright) – (innerright |- boxbottom) – (boxleft |- boxbottom) – cycle;

[anchor=north west, ibmc] at (boxleft |- boxtop) IBMC;

[abox, kind] (innerright |- boxtop) – (kindstartpart |- boxtop) – (ibmcstartpart |- boxtoplower) – (boxtoplower -| boxleft) – (boxleft |- boxbottom) – (insetleft |- boxbottom) – (insetleft |- insettop) – (insettop -| insetright) – (insetright |- boxbottom) – (boxbottom -| boxright) – (boxright |- increment) – (innerright |- increment) – cycle;

[anchor=north east, kind] at (innerright |- boxtop) $k$-induction;

[abox, absint] (boxtop -| innerleft) – (innerleft |- boxbottom) – (boxright |- boxbottom) – (boxright |- boxtop) – cycle;

[anchor=north east, absint, rectangle split, rectangle split parts=2, rectangle split draw splits=false] at (boxright |- boxtop) Abstract second Interpretation;

[merge] (Start) at (start) ;
[stage, rectangle split, rectangle split parts=2, rectangle split draw splits=false] (Init) at (init) Test $\exists \vec{x}_0 \st$ second $\init(\vec{x}_0) \land \serr(\vec{x}_0)$;

[merge] (Initsplit) at (initsplit) ;

[stage, rectangle split, rectangle split parts=3, rectangle split draw splits=false] (Inv) at (inv) Find $\skinv \in \tdom \st \forall \vec{x}_0 , \dots, \vec{x}_k \st$ second
$(\init(\vec{x}_0) \land \sprop[k] \land \strans[k-1] \limplies \sinv[k]) \land$ third
$(\sprop[k] \land \sinv[k] \land \strans[k] \limplies \skinv(\vec{x}_k))$;

[stage, rectangle split, rectangle split parts=2, rectangle split draw splits=false] (Invce) at (invce)
Test $\exists \vec{x}_o , \dots, \vec{x}_k \st$ second $\sprop[k] \land \sinv[k+1] \land \strans[k] \land \serr(\vec{x}_k)$;
[merge] (Invcesplit) at (invcesplit) ;

[stage, rectangle split, rectangle split parts=2, rectangle split draw splits=false] (Concretece) at (concretece)
Test $\exists \vec{x}_0 , \dots, \vec{x}_k \st \init(\vec{x}_0) \land$ second $\sprop[k] \land \sinv[k+1] \land \strans[k] \land \serr(\vec{x}_k)$;
[stage] (Increment) at (increment) $k++$;

[final, starburst] (CE) at (ce) C/E;
[final, cloud, absint, fill=white] (Unknown) at (unknown)  ?;
[final, circle] (Safe) at (safe) Safe;

[link] (kikistart) – (Start.north);

[link] (Start.south) – (Init.north);
[result, right] (k0) at ($(Start.south)!0.5!(Init.north)$) $k:=1$;
[link] (Init.south) – (Initsplit.north);
[result, right] (UNSAT) at ($(Init.south)!0.5!(Initsplit.north)$) UNSAT;

[link] (Initsplit.east) – (Inv.west);

[link] (Inv.south) – (Invce.north);
[link] (Invce.west) – (Invcesplit.east);
[result, below] at ($(Invce.west)!0.5!(Invcesplit.east)$) SAT;

[link] (Invcesplit.west) – (Concretece.east);

[link] (Concretece.north) – (Increment.south);
[result, left] at ($(Concretece.north)!0.5!(Increment.south)$) UNSAT;
[link] (Increment.north) – (Initsplit.south);

[link] (Invce.south) – (Safe.north);
[result, left] at ($(Invce.south)!0.5!(Safe.north)$) UNSAT;
[link] (Concretece.south) – (CE.north);
[result, left] at ($(Concretece.south)!0.5!(CE.north)$) SAT;

[tlink] (Init.west) – (outsidehigh);
[blink] (outsidehigh) – (outsidelow);
[hlink] (outsidelow) – (CE.west);
[result, right] at (outsidehigh |- UNSAT) SAT;

[ibmc, link] (ibmcstart) – (Start);
[ibmc, link] (Initsplit.-60) – (Concretece.17);

[kind, link] (kindstart) – (Start);
[kind, link] (Initsplit.-30) – (Invce.north west);

[absint, link] (absintstart) – (Inv.north);
[absint, link] (Invcesplit.south) – (Unknown);

The  algorithm.

§.§ Template-Based Predicate Inference

A key phase of  is the generation of $\skinv$, a k-inductive invariant.

Perhaps the most obvious approach is to use an off-the-shelf abstract

This works but will fail to exploit the real power of .

In each iteration,  unrolls loops one more step (which can improve the
invariant given by an abstract interpreter) and adds assumptions that previous
unwindings do not give errors.

When directly using a solver, we would need to handle (the
existential fragment of) second-order logic.

As such solvers are not currently available, we reduce to a
problem that can be solved by iterative application of a first-order

We restrict ourselves to finding k-inductive invariants $\kinv$ of the form
$\templ(\vec{x},\vec{\delta})$ where $\templ$ is a fixed expression, a
so-called template, over program variables $\vec{x}$ and
template parameters $\vec{\delta}$.

\begin{equation}\label{equ:invtempl}
\begin{array}{rrl}
\exists \vec{\delta} \st  & \forall \vec{x}_0 \dots \vec{x}_k \st &
\left(\init(\vec{x}_0) \land \strans[k-1] \limplies
\templ[k](\vec{\delta}) \right)
\land \\
&                 &
\left(\templ[k](\vec{\delta})
\land \strans[k] \limplies \templ(\vec{x}_k,\vec{\delta}) \right)
\end{array}
\end{equation}

where $\strans[k]$ is the $k$-th unwinding of the transition relation and
$\templ[k]$ is a template for all states along the unwinding except for the
last state $\vx_k$:

\begin{eqnarray}
\strans[k] = \bigland{i \in [0,k-1]}\trans(\vec{x}_i,\vec{x}_{i+1})
\label{eq:strans}\\
\templ[k](\vec{\delta}) = \bigland{i \in [0,k-1]}
\templ(\vec{x}_i,\vec{\delta}).
\end{eqnarray}

We resolve the
$\exists\forall$ problem by an iterative solving of the negated formula,
particularly of the second conjunct of (<ref>), for different
choices of constants $\vd$ as the values of the parameter $\vdelta$:

\begin{equation}\label{equ:qfinvtempl}
\exists \vec{x}_0 \dots \vec{x}_k \st \neg \big(\templ[k](\vec{d}) \wedge
\strans[k] \limplies \templ(\vec{x}_k,\vec{d})\big).
\end{equation}

The resulting formula can be expressed in quantifier-free logics and
efficiently solved by SMT solvers. Using this as a building block,
one can solve the mentioned $\exists\forall$ problem.

From the abstract interpretation point of view, $\vd$ is an abstract value,
i.e. it represents (concretises to) the set of all program states
$\vs$—here, a state is a vector of values of variables from
$\vx$—that satisfy the formula $\templ(\vs, \vd)$. The abstract
values representing the infimum $\perp$ and supremum $\top$ of the abstract
domain denote the empty set and the whole state space, respectively:
$\equiv \false$ and $\templ(\vs, \top) \equiv
\true$ [4].

Formally, the concretisation function $\gamma$ is:

$\gamma(\vd) = \{ \vs \mid \templ(\vs, \vd) \equiv \true \}.$

In the abstraction function, to get the most precise abstract value representing
the given concrete program state $\vs$,
we let

$\alpha(\vs) = \{ \min(\vd) \mid \templ(\vs, \vd) \equiv \true\}$.

If the abstract domain forms a complete lattice, existence of such
a minimal value $\vd$ is guaranteed.

The algorithm for the invariant inference takes an initial value of $\vd =
\;\perp$ and iteratively solves (<ref>) using an SMT solver.

If the formula is unsatisfiable, then an invariant has been found,
otherwise a model of satisfiability $\vd'$ is returned by the solver. The
model represents a counterexample to the current instantiation of the
template being an invariant. The value of the template parameter $\vd$
is then updated by combining the current value with the obtained model
of satisfiability using a domain-specific join operator [4].

For example, assume we have a program with a loop that counts from 0
to 10 in variable $x$, and we have a template $x\leq d$. Let us assume
that the current value of the parameter $d$ is $3$, and we get a new
model $d'=4$.  Then we update the parameter to $4$ by computing $d
\sqcup d' = \max(d, d')$, because $\max$ is the join operator for
a domain that tracks numerical upper bounds.

In 2LS, we use a single template to compute all invariants of the analysed

Therefore, typically, a template is composed of multiple parts, each part
describing an invariant for a set of program variables.

With respect to this, we expect a template $\templ(\vx, \vdelta)$ to be composed
of so-called template rows $\templ_r(\vx_r, \delta_r)$, each row $r$
describing an invariant for a subset $\vx_r$ of variables $\vx$ and having its
own row parameter $\delta_r$.

The overall invariant is then a composition of individual template rows with
computed values of the corresponding row parameters.

The kind of the composition (it can be, e.g., a simple conjunction) is defined
by each domain.

§.§.§ Guarded Templates
Since we use the SSA form rather than control
flow graphs, we cannot use templates directly.

Instead we use guarded templates.

As described above, a template is composed of multiple template rows, each row
describing an invariant for a subset of program variables.

In a guarded template, each row $r$ is of the form $G_r(\vx_r) \limplies
\basetempl_r(\vx_r,\delta_r)$ for the $r^{\text{th}}$ row $\basetempl_r$ of the
base template domain (e.g.  template polyhedra).

$G_r$ is the conjunction of the SSA guards $g_r$ associated with the definition
of variables $\vx_r$ occurring in $\basetempl_r$.

Since we intend to infer loop invariants, $G_r(\vx_r)$ denotes the guard
associated to variables $\vx_r$ appearing at the loop head.

Hence, template rows for different loops have different guards.

We illustrate the above on the example program in Figure <ref>
using a guarded interval template.

The template has the form:
\begin{equation}\label{eq:ex_templ}
\templ(\ssaxlb{6},(\delta_1,\delta_2)) = \begin{array}{lcr} \ssag{3} \wedge
\ssagls{6} &\limplies & \ssaxlb{6} \leq \delta_1 \;\wedge\\[0.3em] \ssag{3}
\wedge \ssagls{6} &\limplies & -\ssaxlb{6} \leq \delta_2.  \end{array}
\end{equation}

Here, $\ssag{3}$ and $\ssagls{6}$ guard the definition of
$\ssaxlb{6}$—$\ssag{3}$ expresses the fact that the loop head is reachable and
$\ssagls{6}$ expresses that $\ssaxlb{6}$ is chosen as the value of

§.§.§ Solving of the $\exists\forall$ Problem

As discussed above, it is necessary to solve an $\exists\forall$ problem to
find values for template parameters $\vec{\delta}$ to infer invariants.

§.§.§ Model enumeration

The well-known method [31, 5] for solving this problem
in (<ref>) using an SMT solver is to repeatedly check
satisfiability of the formula for different abstract values $\vec{d}$ (starting
with the infimum $\vec{d}=\bot$):

\begin{equation}\label{equ:indcheck}
\templ[k](\vec{d}) \land \strans[k] \wedge \neg
\templ(\vec{x}_k,\vec{d}).
\end{equation}

If it is unsatisfiable, then we have found an invariant; otherwise, we join the
model returned by the solver with the previous abstract value $\vec{d}$ and
repeat the process with the new value of $\vd$ obtained from the join.

This method corresponds to performing a classical Kleene iteration on the
abstract lattice up to convergence.

Convergence is guaranteed because our abstract domains are finite.

However, while this method might be sufficient for some abstract domains
(especially those with a low number of possible states), it is practically
unusable for other ones.

For example, when dealing with integer variables, the height of the lattice is
enormous and even for a one-loop program incrementing an unconstrained 64-bit
variable, the naïve algorithm will not terminate within human life time.

Hence, for some abstract domains, we are going to use an optimised method
(e.g., for some numerical domains, see Section <ref>).

In general, there may be a specific method for solving the $\exists\forall$
problem for each domain.

We refer to these methods as to domain strategy iterations.

§.§.§ Generic domain strategy iteration

Even though each domain may implement its own strategy iteration algorithm, we
observe that all algorithms are to some extent similar.

This is related to the fact that abstract domain templates are typically
composed of multiple template rows, as described earlier in this section.

With respect to this, we developed a generic strategy iteration
algorithm [26] parametrised by an abstract domain having the form
of a template.

The algorithm is shown in Figure <ref>.

[1]
$\vd \gets \perp$
$\templ[k](\vd)$ is not an invariant
solver $\gets \templ[k](\vd)$
solver $\gets \neg \templ(\vx_k, \vd)$
solver.solve() $=$ SAT
$\templ_r(\vx_r, d_r) \in \templ(\vx, \vd)$
$m_r \gets$ solver.model($\vx_r$)
find $d_m$ s.t. $\templ_r(m_r, d_m)$ holds
$d_r \gets d_r \sqcup d_m$

Generic strategy iteration algorithm for solving the $\exists\forall$

The algorithm repeatedly solves (<ref>) for the given
abstract domain.

If the formula is satisfiable, then for each template row $r$, the algorithm
gets the model of satisfiability for the variables that $r$ describes.

The obtained model (i.e., the values of the concerned variables) is used to
instantiate the template row formula (line 8) and the corresponding value of
the template parameter is joined with the previous value of the row parameter.

Since 2LS uses incremental solving, we assume that the transition relation
(expressed by the SSA form) is already a part of the solver clause set.

Moreover, formulae added to the solver clause set on lines 3 and 4 are removed
after each iteration.

This ensures efficiency of the method since only the new formulae need to be
re-solved every time.

However, as we mentioned in the previous section, an optimisation may be
required in order to assure scaling of the algorithm.

In such case, lines 7-9 are replaced by the optimised method for
determining values of template row parameters.

We will give an example for such optimised techniques in
Section <ref>.

§.§ Incremental Bounded Model Checking

Bounded Model Checking (BMC) [2]
focuses on refutation by picking an
unwinding limit $k$ and solving the equation

\begin{equation}\label{eq:bmc}
\exists \vec{x}_0, \dots, \vec{x}_k \st \init(\vec{x}_0) \land
\strans[k]
\land
\lnot \sprop[k+1]
\end{equation}

where $\strans[k]$ is an unwound transition relation as defined
by (<ref>) and $\sprop[k]$ is a predicate stating that $k$ states are

\begin{equation}
\sprop[k]  = \bigland{i \in [0,k-1]} \lnot \err(\vec{x}_i).
\end{equation}

Models of (<ref>) correspond to concrete
counterexamples of some length $n \lte k$.  The unwinding limit gives
an under-approximation of the set of reachable states and thus
can fail to find counterexamples that take a large number of
transition steps.  In practice, BMC works well as the formula is
existentially quantified and thus is in a fragment handled well by SAT
and SMT solvers.

Incremental bounded model checking is one of the core components
of the algorithm presented in Section <ref>.

It corresponds to the red part in Figure <ref>.

Incremental BMC (IBMC) (e.g. [13]) uses repeated BMC checks (often
optimised by using the solver incrementally) with increasing
bounds to avoid the need for a fixed bound.

If the bound starts at 0
(i.e. checking $\exists x_0 \st \init(\vec{x}_0) \land
\err(\vec{x}_0)$) and is increased by one in each step (this is the common
use-case), then it can be assumed that there are no errors at previous
states, giving a simpler test:

\begin{equation}
\exists \vec{x}_0, \dots, \vec{x}_k \st
\init(\vec{x}_0) \land
\strans[k] \land \sprop[k]
\land
\err(\vec{x}_k).
\end{equation}

In Section <ref>, we will discuss how incremental BMC
can be implemented efficiently using incremental SAT solving.

§.§ Incremental $k$-Induction

Incremental $k$-induction [36] is the blue part of the algorithm
in Figure <ref>.

It can be viewed as an extension of IBMC
that can show system
safety as well as produce counterexamples.  It makes use of
$k$-inductive invariants, which are predicates that have the
following property:

\begin{equation}
\forall \vec{x}_0 \dots \vec{x}_k \st \sinv[k] \land \strans[k] \limplies \kinv(\vec{x}_k)
\end{equation}

\begin{equation*}
\sinv[k] = \bigland{i \in [0,k-1]} \kinv(\vec{x}_i).
\end{equation*}

$k$-inductive invariants have the following useful properties:

* Any inductive invariant is a $1$-inductive invariant and vice versa.

* Any $k$-inductive invariant is a $(k+1)$-inductive invariant.

* A (finite) system is safe if and only if there is a $k$-inductive
invariant $\kinv$ which satisfies:

\begin{equation}
\begin{array}{rrl}
& \forall \vec{x}_0 \dots \vec{x}_k \st &
\left(\init(\vec{x}_0) \land \strans[k] \limplies \sinv[k] \right)
\land \\
&                 &
\left(\sinv[k] \land \strans[k] \limplies \kinv(\vec{x}_k)\right)
\land \\
&                 &
\left(\kinv(\vec{x}_k) \limplies \lnot \err(\vec{x}_k)\right).
\end{array}
\end{equation}

Showing that a $k$-inductive invariant exists is sufficient to
show that an inductive invariant exists but it does not imply
that the $k$-inductive invariant is an inductive invariant.  Often
the corresponding inductive invariant is significantly more complex.
Thus $k$-induction can be seen as a trade-off between
invariant generation and checking
as it is a means to benefit as much as possible from
simpler invariants by using a more complex property check.

However, finding a candidate $k$-inductive invariant is still hard, and so
implementations often use $\lnot \err(\vec{x})$ as the candidate. Similarly to
IBMC, linearly increasing $k$ can be used to simplify the expression by
assuming there are no errors at previous states:

\begin{equation}
\begin{array}{rrl}
& \exists \vec{x}_0, \dots, \vec{x}_k \st &
(\init(\vec{x}_0) \land \strans[k] \land \sprop[k] \land \err(\vec{x}_k)) \lor\\
&                 &
(\strans[k] \land \sprop[k] \land \err(\vec{x}_k)).
\end{array}
\end{equation}

A model of the first part of the disjunct is a concrete
counterexample ($k$-induction subsumes IBMC) and if the whole
formula has no models, then $\lnot \err(\vec{x})$ is a $k$-inductive
invariant and the system is safe.

§.§ Incremental SAT Solving

2LS requires incremental back-end solvers.

The first ideas for incremental SAT solving date back to the 1990s
[19, 37, 20].  The question is how to solve a sequence
of similar SAT problems while reusing the effort spent on solving previous
instances.  The authors of [38, 39] identify conditions for the
reuse of learnt clauses, but this requires expensive book-keeping, which
partially saps the benefit of incrementality.

Obviously, incremental SAT solving is easy when the modification to
the CNF representation of the problem makes it grow monotonically.

This means that if we want to solve a sequence of (increasingly
constrained) SAT problems with CNF formulae $\Phi(k)$ for $k\geq 0$,
then $\Phi(k)$ must be growing monotonically in $k$, i.e.,
$\Phi(k+1) = \Phi(k) \wedge \varphi(k)$ for CNF formulae $\varphi(k)$.

Removal of clauses from $\Phi(k)$ is trickier as some of the clauses
learnt during the solving process are no longer implied by the new
instance and need to be removed as well.

This requires additional solver features like solving under
assumptions [13], which is the most popular approach to
incremental SAT solving: assumptions are temporary assignments to variables
that hold solely for one specific invocation of the SAT solver.

We will see that incremental BMC requires
a non-monotonic series of formulae.

An alternative approach is to use SMT solvers.

SMT solvers offer an interface for pushing and popping clauses in a stack-like
manner. Pushing adds clauses, popping removes them from the formula.

This makes the modification of the formula intuitive to the user, but the
efficiency depends on the underlying implementation of the push and pop

For example, in [17], it was observed that some SMT solvers (like Z3) are
not optimised for incremental usage and hence perform worse incrementally than

Consequently, since the support for incremental solving in SMT solvers is still
lagging behind in comparison to SAT solvers, we use SAT solving.

The CPROVER framework [8] itself implements powerful
bitvector decision procedures that use a SAT solver such as
[12] or Glucose

as the backend solver.  For SAT solvers, solving under assumptions is the
prevalent method.

§.§.§ Formula construction in incremental BMC

Following the construction in [13] (stated for finite state machines),
incremental BMC can be formulated as a sequence of SAT problems
$\Phi(k)$ that we need to solve:

\begin{equation}\label{equ:incrbmc}
\begin{array}{lcl}
\Phi(0) &:=& \init(\vec{x}_0) \wedge (\alpha_0 \Rightarrow \err(\vec{x}_0))\\
&& \text{with the assumption }\alpha_0,\\
\Phi(k+1) &:=& \Phi(k) \wedge \neg \err(\vec{x}_k) \wedge \trans(\vec{x}_k,\vec{x}_{k+1})  \wedge \neg \alpha_k
\wedge (\alpha_{k+1} \Rightarrow \err(\vec{x}_{k+1}))\\
&& \text{with the assumption } \alpha_{k+1}\\
\end{array}
\end{equation}

where $\alpha_k$ are Boolean variables.

Let us now take a look why these are necessary.

Consider a program counting in variable $x$ from 0 to 10.

There is an assertion inside the loop that $x\leq 1$ is expected to hold. We
start with the initial formula (omitting Boolean variables $\alpha_k$):

\Phi(0) := (x_0{=}0) \wedge (x_0{<}10)\wedge (x_1{=}x_0+1)\wedge \neg(x_1{\leq}1).

This formula is UNSAT. We now (naïvely) extend the formula with the next
loop iteration:

\Phi(1) := (x_0{=}0) \wedge (x_0{<}10)\wedge (x_1{=}x_0{+}1)\wedge \neg(x_1{\leq}1)
\wedge (x_1{<}10)\wedge (x_2{=}x_1{+}1)\wedge \neg(x_2{\leq}1).

This is still UNSAT, although we expect it to be SAT. Obviously, the reason is
that we are adding further conjuncts to something that is already UNSAT.
Therefore, in order to be sound, we have to remove $x_1>1$ from the previous
iteration, which makes the formula construction non-monotonic.

However, as explained above, we cannot
simply remove parts of the formula from the solver, but
we can solve this issue with the help of solving under assumptions.

In iteration $k$, the assumption $\alpha_k$ is assumed to be true, whereas
it is assumed false for iterations $k'>k$. This has the effect that,
in iteration $k'$, the sub-formula $(\alpha_k \Rightarrow \err(\vx_k))$
becomes trivially satisfied. Hence, it does not contribute to the
(un)satisfiability of $\Phi(k')$, which emulates its deletion.
[For a large number of iterations $k$, such
trivially satisfied subformulas might accumulate as “garbage” in the
formula and slow down its resolution. Restarting the solver
at appropriate moments is the common solution to this issue [6].]

§.§.§ The Benefit of Incremental BMC

The benefit of incremental BMC: solving time vs. overall runtime
(explanation in the text).

Non-incremental BMC has to perform extra work in symbolic execution
for each unwinding $k$.

As investigated in [35],
one might argue that removing this overhead is the main reason why
incremental BMC is faster.

However, the overhead for symbolic execution when compared to generating and
solving a SAT formula is similar for the incremental and non-incremental

on the embedded software benchmark set of [35],
27 % of the time taken by the incremental approach are spent in
solving SAT formulae (582 out of 2,151 seconds), compared with 28 %
of the time taken by the non-incremental approach (3,317 out of 11,811

We illustrate this observation in the bar chart in
Fig. <ref>, which plots the total runtime consisting of
the time spent in generating SAT formulae and solving them (light
grey) and the overhead (dark grey) for incremental and non-incremental

Unsurprisingly, as shown in the third bar in Fig. <ref>,
solving the instance for the largest $k$ in the non-incremental
approach (white) takes a considerable amount of time (around 24 %),
when compared to the total time (white+grey) for solving the SAT
formulae for iterations 1 to $k$ (784 out of 3,317 seconds).

An explanation for the speedups achieved by incremental BMC might be
the size of the queries issued in both approaches.  The average number
of clauses per solver call is halved from 1,367k clauses for the
non-incremental approach to 709k clauses for the incremental
approach. Similarly, the average number of variables of the last call
is less than a third in the incremental approach when compared to the
non-incremental approach, being 217k and 746k respectively.  That
means that the SAT solver is able to simplify the formulae within
pre-processing much more efficiently in the incremental approach.

The work [35] experimented with an incremental slicing algorithm in
combination with incremental unwinding in ; however, this is not
implemented .

The work [30] developed an SMT solving algorithm in 2LS (which
is available in a prototype branch of 2LS) that uses template polyhedra
instead of Boolean literals in order to perform theory-level propagation based
on the concept of Abstract Conflict Driven Learning [11].

§ IMPLEMENTED ANALYSES

2LS supports analysis of various program features such as reachability of
assertions, termination, or memory safety. For most of these analyses, 2LS
introduces abstract domains [10] for invariant inference, which is one of the steps
of the algorithm.

There are numerical domains such as template polyhedra (see
Section <ref>), equalities and disequalities, domains for
ranking functions (see Section <ref>) and recurrent
sets(see Section <ref>), and domains for the shape of
data structures (see Section <ref>).

In this section, we introduce the most important supported abstract domains as
well as other concepts that support verification of various program properties.

§.§ Template Polyhedra Abstract Domain

Template polyhedra [32] are
a class of templates for numerical variables which have the form
$\templ = (\mathbf{A}\vec{x}\leq\vec{\delta})$ where
$\mathbf{A}$ is a matrix with fixed coefficients.

Subclasses of such templates include Intervals,
which require constraints $\vecv{1}{-1}x_i\leq\vecv{\delta_{i1}}{\delta_{i2}}$

for each variable $x_i$, Zones (differences), and
Octagons [28].

The $r^{\textit{th}}$ row of the template are the constraints
generated by the $r^{\text{th}}$ row of matrix $\mathbf{A}$.

In our template expressions, variables $\vec{x}$ are
bit-vectors representing signed or unsigned integers.

These variables can be mixed in template constraints. Type promotion
rules are applied such that the bit-width of the types of the
expressions are extended in order to avoid arithmetic under- and
overflows in the template expressions.

$\top$ corresponds to the respective maximum values in the promoted
type, whereas $\bot$ must be encoded as a special symbol.

§.§.§ Optimised Solving of the $\exists\forall$ Problem

In order to solve the parameter synthesis problem efficiently, we need a
convergence acceleration that makes the computational effort independent
from the number of states and loop iterations.

To this end, we use a technique that is inspired by an encoding used by
max-strategy iteration methods [15, 14, 29].

These methods state the invariant inference problem over template polyhedra as a
disjunctive linear optimisation problem, which is solved iteratively by an
upward iteration in the lattice of template polyhedra:

using SMT solving, a conjunctive subsystem (“strategy”) whose
solution extends the current invariant candidate is selected.  This
subsystem is then solved by an LP solver; the procedure terminates as
soon as an inductive invariant is found.[
Intuitively, this works as follows: As an example,
assume the domain of upper bounds on numerical variables (but the
approach extends to any domain satisfying the conditions mentioned
further below). An invariant upper bound at a program location is
then the maximum value contributed by any of the incoming
transitions to the program location. Writing this down as an
optimisation problem over a system of linear inequalities, incoming
transitions form disjunctions. Considering multiple program
locations we get conjunctions of these disjunctions. So, we have a
linear system in the CNF form. This can be solved by finding those
disjuncts (i.e., incoming transitions) in each clause that are
satisfied by the initial state (there must be such, otherwise the
system is not feasible). We can then pick these disjuncts and
conjoin them (as the “strategy”), resulting in a (conjunctive)
linear system (called a conjunctive subsystem), which can be solved
using an LP solver. The obtained upper bound is only valid for those
disjuncts that have been picked. If it is not an invariant yet, then
there must be disjuncts that can be substituted for some of the
disjuncts to improve the bound. This can be repeated and is
guaranteed to terminate with the minimal invariant.]

The above method can only be used if the domain is convex and the parameter
values are ordered and monotonic w.r.t. concretisation, which holds true, for
example, for template polyhedra $\mathbf{A}\vec{x}\leq\vec{d}$ where $\vec{d}$
is a parameter but not for those where $\mathbf{A}$ is a parameter.

If the operations in the transition relation satisfy certain properties such as
monotonicity of condition predicates, then the obtained result is the least
fixed point, i.e. the same result as the one returned by the naïve
model enumeration above but much faster on average.

We adapt this method to our setting with bit-vector variables and
guarded templates. Since we deal with finite domains (bit-vectors), we
can use binary search as an optimisation method instead of an LP solver.

The algorithm proceeds as follows:

We start by checking whether the current abstract value $\vec{d}$ (starting from
$\vec{d}=\bot$) is inductive (see (<ref>)). If so, we have found an
invariant; otherwise there are template rows $R$ whose values are not inductive

Moreover, the counterexample to induction obtained from the inductivity
check tells us which bounds need to be improved.

We construct the system

\begin{equation}\label{equ:symbsys}
\bigland{i \in [0,k-1]} \left\{\begin{array}{rll}
& \bigwedge_{r\notin R} & G_r(\vec{x}_i) \limplies (\rowexpr_r(\vec{x}_i)\leq d_r) \\[1ex]
\wedge & \bigwedge_{r\in R} & G_r(\vec{x}_i) \limplies (\rowexpr_r(\vec{x}_i)\leq \delta_r)\\[1.5ex]
\end{array}\right\}
\wedge \strans[k]
%\wedge \trans(\vec{x}_0,\vec{x}_k)
\wedge \bigwedge_{r\in R} (G_r(\vec{x}_k) \wedge \delta_r\leq \rowexpr_r(\vec{x}_k))
\end{equation}

where $\rowexpr_r$ is the left-hand side of the inequality
corresponding to the $r^\text{th}$ row of the template.

Then we start the binary search for the minimal value of $\sum_{r\in R}\delta_r$
over this system.

The initial bounds for $\sum_{r\in R}\delta_r$ are as follows:

* The lower bound $\ell$ is $\sum_{r\in R} d'_r$ where $d'_r$ is the
value of $\rowexpr_r(\vec{x}_k)$ in the model of the inductivity
check (<ref>) above;

* The upper bound $u$ is $\sum_{r\in R}\mathit{max\_value}(r)$ where
$\mathit{max\_value}$ returns the maximum value that $\rowexpr_r(\vec{x}_k)$
may have (dependent on variable type).

The binary search is performed by iteratively checking (<ref>) for
satisfiability under the assumption
$\sum_{r\in R}\delta_r\geq m$ where $m = \mathit{median}(\ell,u)$.  If
satisfiable, set $\ell := m$, otherwise set $u := m$ and repeat until
$\ell = u$.

The values of $\delta_r$ in the last satisfiable query are assigned to
$d_r$ to obtain the new abstract value.
The procedure is then repeated by testing whether $\vec{d}$ is
inductive (<ref>).

Note that this algorithm uses a similar encoding for bound
optimisation as strategy iteration, but it potentially requires a higher
number of iterations than strategy iteration.  This choice has been
made deliberately in order to keep the size of the generated SMT
formulas small, at the cost of a potentially increased number of

The same row $r$ may be removed from $R$ and improved again in
later iterations. However, as each iteration makes progress,
the algorithm terminates in a finite number of iterations.

We illustrate the binary search
algorithm on the example from Figure <ref>.

We use the interval abstract domain to compute the inverval for the value of the
variable $x$ at the end of the loop.

We let $k = 1$, and therefore we let $\vx_0 = (\ssaxlb{6})$ and $\vx_1 =
(\ssax{5})$.[Variables $\vx_0$ apply to the case of zero
iterations of the loop, hence unconstrained $\ssaxlb{6}$ is taken here as the
value of $x$.]

The corresponding guarded template $\templ$ has the form defined
in (<ref>).

The template contains two template rows defined as:
\begin{eqnarray} &
G_0(\ssaxlb{6}) \limplies \ssaxlb{6} \leq \delta_0 \\ & G_1(\ssaxlb{6})
\limplies -\ssaxlb{6} \leq \delta_1 \end{eqnarray}
where $G_0(\ssaxlb{6}) =
G_1(\ssaxlb{6}) = \ssag{3} \wedge \ssagls{6}$.

We also define the template row guards for variables $\vx_1$ (corresponding to
the values of the program variables after one execution of the transition
relation) as $G'_0(\ssax{5}) = G'_1(\ssax{5}) = \ssag{5} = \ssaxphi{3} < 10$.

Initially, $\vd = \perp$, and we solve (<ref>).

Since using $\vd = \perp$ as the value of the parameters makes the
instance of the template $\false$ by definition, the invariant cannot be
inductive, and we get a model of satisfiability.

Neither of the template rows is inductive, and hence we
instantiate (<ref>) with $R = \{0, 1\}$.

The obtained system of formulae is the following (with $\trans(\vx_0,
\vx_1)$ being the conjunction of the constraints shown in
Fig. <ref>(b)):

\begin{equation}
\begin{split}
G_0(\ssaxlb{6}) \limplies \ssaxlb{6} \leq \delta_0 ~\wedge \\
G_1(\ssaxlb{6}) \limplies -\ssaxlb{6} \leq \delta_1 ~\wedge \\
\trans(\vx_0, \vx_1) ~\wedge \\
G'_0(\ssax{5}) \wedge \delta_0 \leq \ssax{5} ~\wedge \\
G'_1(\ssax{5}) \wedge \delta_1 \leq -\ssax{5}. \\
\end{split}
\end{equation}

We apply binary search to the system starting with $\ell = -2^{31}$ and $u =
2^{31} - 1$.

We get $\delta_0 = 1$ and $\delta_1 = -1$.

Now, template row 1 ($-\ssaxlb{6} \leq -1$) is inductive, however,
template row 0 is not inductive.

We construct a new system as per (<ref>) with $R = \{0\}$:

\begin{equation}
\begin{split}
G_0(\ssaxlb{6}) \limplies \ssaxlb{6} \leq \delta_0 ~\wedge \\
G_1(\ssaxlb{6}) \limplies -\ssaxlb{6} \leq -1 ~\wedge \\
\trans(\vx_0, \vx_1) ~\wedge \\
G'_0(\ssax{5}) \wedge (\delta_0 \leq \ssax{5}).
\end{split}
\end{equation}

Using binary search, we get $\delta_0 = 10$.

With this, template row 0 is inductive, and so we have found an
invariant, namely:

\begin{equation}
\begin{split}
& \ssag{3} \wedge \ssagls{6} \limplies \ssaxlb{6} \leq 10 ~\wedge \\
& \ssag{3} \wedge \ssagls{6} \limplies -\ssaxlb{6} \leq -1.
\end{split}
\end{equation}

§.§.§ Bitvector Width Extension

Integers wrap around on most architectures when
they over/underflow. Thus, we have to be mindful of these in
arithmetic within templates in order to guarantee soundness of the results.

Let us consider an example of analysing termination of the following function
by synthesising a ranking function.

void f()
signed char x;
while(1) x++;

The ranking function synthesis aims to compute a value for a template
parameter $\rankparam$ such that $\rankparam(x{-}x')>0$ holds for all $x,
x'$ under the transition relation $x'{=}x{+}1$ and the computed invariant $\true$.

Thus, assuming that the current value for $\rankparam$ is $-1$, the
constraint to be solved is

\[ \true \wedge x'{=}x{+}1 \wedge \neg({-1}\cdot(x{-}x'){>}0), \]

which is equivalent to $\neg({-1}(x{-}(x{+}1)){>}0)$.

While for mathematical integers this is satisfiable, it is unsatisfiable for
signed bit-vectors due to overflows.  For $x{=}127$, the overflow happens
such that $x{+}1{=}{-}128$ if  is an 8-bit signed integer.

Thus, $\neg(-1 \cdot (127{-}({-}128)){>} 0)$ becomes $\neg (1 {>} 0)$,
which makes the constraint unsatisfiable, and we would incorrectly conclude
that $-x$ is a ranking function, which does not hold for signed bitvector
semantics.  However, if we extend the bitvector width to $k{=}9$ such that
the arithmetic in the template does not overflow, then
evaluates to $\neg((-1 \cdot 255)>0)$, where $\mathit{signed}_k$ is a cast to a $k$-bit
signed integer.

Now, $x{=}127$ is a model that shows that $-x$ is not a valid ranking

For these reasons to retain soundness, we extend the bit-width of
signed and unsigned integer operands to integers that can hold the
result of the operation without over- or underflow, e.g., one
additional bit for additions and doubling the size plus one bit for

The maximum bit-width required depends on the shape of the
template. Since our templates contain a finite number of operations,
the maximum bit-width is finite.

Floating-point numbers do not require extensions as they overflow
(resp. underflow) to infinity (resp. minus infinity), which does not
impact soundness.

§.§ Termination Analysis

For reasoning about termination, we need the notions of ranking
functions and preconditions for termination.

A ranking function for a procedure $(\init,$ $\trans)$
is a function $r$ such that

\[
\begin{array}{rlr}
\multicolumn{2}{l}{\exists \Delta>0, \inv: \forall \vx, \vxp:} \\
& \left(\init(\vx) \Longrightarrow \inv(\vx)\right)
\\
\wedge & \left(\inv(\vx)\wedge\trans(\vx,\vxp)\Longrightarrow \inv(\vxp)
\wedge r(\vx) {-} r(\vxp) {>} \Delta \wedge r(\vx) {>} 0\right).
\end{array}
\]

Thus, $r$ is a function from the set of program states to a well-founded domain, e.g. $\mathbb{R}^{\geq 0}$.

We denote by $\rrank(\vx,\vxp)$ the constraints on $r$ that form the
termination argument, i.e., $r(\vx) - r(\vxp) > \Delta \wedge r(\vx) >
0$ for monolithic ranking functions.

The existence of a ranking function for a procedure guarantees its
universal termination.

Monolithic ranking functions are complete, i.e., termination can always be
proven monolithically if a program terminates.  However, in practice,
combinations of linear ranking functions, e.g., linear lexicographic

are preferred.  This is driven by the fact that
monolithic linear ranking functions are not expressive enough, and
that non-linear theories are challenging for the existing SMT
solvers, which handle the linear case much more efficiently.

A lexicographic ranking function $R$
for a procedure $(\init, \trans)$ is an

$n$-tuple of expressions $(\rank_n, \rank_{n-1}, \ldots,\allowbreak \rank_1)$ such

\begin{array}{rllr}
\multicolumn{3}{l}{\exists \Delta>0, \inv: \forall \vx, \vxp:} \\
& \multicolumn{2}{l}{\left(\init(\vx) \Longrightarrow \inv(\vx)\right)}\\
\wedge & \multicolumn{2}{l}{\big(\inv(\vx)\wedge
\trans(\vx,\vxp)\Longrightarrow \inv(\vxp)
\wedge \exists i\in [1,n]:}\\
&& \rank_i(\vx) > 0 & \text{(Bounded)} \\
&~~~~\wedge & \rank_i(\vx) - \rank_i(\vxp) > \Delta & \text{(Decreasing)} \\
&~~~~\wedge & \forall j>i: \rank_j(\vx) - \rank_j(\vxp) \ge 0~\big) &
\qquad\text{(Non-increasing)}.
\end{array}

Notice that this is a special case of
Definition <ref>.  In particular, the existence
of $\Delta>0$ and the Bounded condition guarantee that $>$ is a
well-founded relation.

Before we encode the requirements for lexicographic ranking functions into
constraints, we need to optimise them to take advantage of bit-vector
semantics.  Since bit-vectors are bounded, it follows that the
Bounded condition is trivially satisfied and therefore can be
omitted.  Moreover, bit-vectors are discrete, hence we can replace the
Decreasing condition with $\rank_i(\vx)-\rank_i(\vxp)>0$.  The
following formula, $\lexrank^n$, holds if and only if $(\rank_n, \rank_{n-1},
\ldots, \rank_1)$ is a lexicographic ranking function with $n$ components over

\[
\lexrank^n(\vx,\vxp) =
\bigvee_{i=1}^{n} \left(\rank_i(\vx)-\rank_i(\vxp)>0 \; \wedge
\bigwedge_{j=i+1}^{n}(\rank_j(\vx)-\rank_j(\vxp)\geq 0)\right)
\]

Assume we are given the transition relation $\trans(\vx,\vxp)$ of a
procedure $f$.  The procedure $f$ may be composed of several
loops, and each of the loops is associated with guards $g$ (and $g'$)
that express the reachability of the loop head (and the end of the
loop body, respectively; see Section <ref>).

That is, suppose $f$ has $k$ loops
and $n_i$ denotes the number of lexicographic components for loop $i$,
then the termination argument
to prove termination of $f$ takes the form:

\[
\rrank^{\vec{n}}(\vx,\vxp) = \bigwedge_{i=1}^{k} g_i\wedge g'_i \Longrightarrow \lexrank^{n_i}_i(\vx,\vxp)
\]

While ranking techniques for mathematical integers use, e.g., Farkas' Lemma,
this is not applicable to bitvector operations. Thus, we use a synthesis

and extend it from
monolithic to lexicographic ranking functions.

We consider the class of lexicographic ranking functions generated by
the template where $\rank_i(\vx)$ is the product
$\vec{\rankparam}_i \vx$ with the row vector $\vec{\rankparam}_i$
of template parameters.

We denote the resulting constraints for loop $i$ as
$\lexranktempl_i^{n_i}(\vx,\vxp,\rankparamvec_i^{n_i})$ where
$\rankparamvec_i^{n_i}$ is the vector

The constraints for the ranking functions of a whole procedure are
$\rranktempl(\vx,\vxp,\vec{\rankparamvec}^{\vec{n}})$, where
$\vec{\rankparamvec}^{\vec{n}}$ is the vector

Putting all this together, we obtain the following reduction of ranking
function synthesis to a first-order quantifier elimination problem over

\exists \vec{\rankparamvec}^{\vec{n}}: \forall \vx,\vxp:
\inv(\vx)\wedge\trans(\vx,\vxp) \Longrightarrow \rranktempl(\vx,\vxp,\vec{\rankparamvec}^{\vec{n}})

The parameters $\rankparamvec_i^{n_i}$ are vectors of vectors of bitvectors
extended by the special value $\top$ in order
to complete the lattice of ranking constraints

We define $\lexranktempl_i^{n_i}(\vx,\vxp,\top) \eqdef \true$
indicating that no ranking function has been found for the given
template (“don't know”).

We write $\bot$ for the equivalence class of bottom elements for which
evaluates to $\false$, meaning that the ranking function has not yet
been computed. For example, $\vec{0}$ is a bottom element.

Note that this intuitively corresponds to the meaning of $\bot$ and
$\top$ as known from invariant inference by abstract interpretation
(see Section <ref>).

The algorithms for solving these formulae are described in
detail in [7].

Moreover, [7] explains algorithms for conditional
termination, i.e. programs that terminate only when certain
conditions on their inputs hold. The objective is to determine
these conditions.

Also, an approach to modular termination analysis using
procedure-level summaries is described in [7].
2LS has an experimental implementation for these algorithms.

The works [7, 33] investigate how to solve approximate
solutions to these inter-procedural formulae that result
from modular analysis. Moreover, the works [7, 21] also look into
under-approximating backwards analysis in an inter-procedural

§.§ Non-Termination Analysis

2LS implements two techniques for proving
non-termination [24, 25].

Both of the approaches are relatively  simple, yet appear to be reasonably
efficient in many practical cases.

The first approach is based on finding singleton recurrent sets.

All loops are unfolded $k$ times (with $k$ being incrementally
increased), followed by a check whether there is some loop $L$ and a program
configuration that can be reached at the head of $L$ after both $k'$ and $k$
unwindings for some $k' < k$.

Such a check can be easily formulated in 2LS as a formula over the SSA
representation of programs with loops unfolded $k$ times.

This technique is able to find lasso-shaped executions in which a loop
returns to the same program configuration every $k-k'$ iterations
after $k'$ initial iterations.

The second approach tries to reduce the number of unwindings by looking for
loops that generate an arithmetic progression over every integer

More precisely, it looks for loops $L$ for which each integer variable
$x$ can be associated with a constant $c_x$ such that every iteration
of $L$ changes the value of $x$ to $x+c_x$, keeping non-integer
variables unchanged.

Two queries are used to detect such loops: the first one asks whether
there is a configuration $\overline{x}$ and a constant vector
$\overline{c}$ (with the vectors ranging over all integer variables
modified in the loop and constants from their associated bitvector
domains) such that one iteration of $L$ ends in the
configuration $\overline{x}+\overline{c}$, while the second makes sure
that there is no configuration $\overline{x}'$ over which one
iteration of $L$ would terminate in a configuration other than

If such a loop $L$ and a constant vector $\overline{c}$ are found,
non-termination of $L$ can be proved as follows:

First, we gradually exclude each configuration $\overline{x}$
reachable at the head of $L$ for which there is some $k$ such that $L$
cannot be executed from $\overline{x}+k.\overline{c}$ (intuitively
meaning that $L$ cannot be executed $k+1$ times from $\overline{x}$).

Second, we check whether there remains some non-excluded configuration
reachable at the head of $L$.

The termination and non-termination analyses are run in parallel, and
the first definite answer is used.

Among the non-termination analyses, several rounds of unwinding
are first tried with the singleton recurrence set approach.

If that is not sufficient, the arithmetic progression approach is

If that does not succeed either, further rounds of unwinding with the
former approach are run.

§.§ Memory Safety

Analysing memory safety requires reasoning about values of pointers and about
the shape of the program heap. To this end, we introduce an abstract domain for
heap analysis—a so-called abstract shape domain [22]. Memory
safety analysis is based on computing invariants in this domain and then
automatically generating assertions checking for absence of memory safety
errors, such as $\nullptr$ pointer dereference.

§.§.§ Abstract Domain for Heap Analysis

Similarly to all abstract domains in 2LS, the abstract shape domain has a form
of a template describing the desired property. The shape of the heap is
defined by pointer links among memory objects and therefore our shape domain is
limited to the set $\ptr$ of all pointers defined by (<ref>).
More particularly, since the shape domain is used to infer loop invariants, we
limit it to the set $\ptr^{lb}$ of all loop-back pointers.

Let $L$ be the set of all loops in the analysed program. We define

\begin{equation}
\ptr^{lb} = \ptr \times L.
\end{equation}

Elements of this set represent abstractions of values of individual pointers
returning from the end of loop bodies that are introduced in our program
representation (see Section <ref>).  We denote loop-back pointers $(p,
l) \in \ptr^{lb}$ by $\ssalb{p}{i}$ where $i$ is the program location of the
end of the loop $l$.

The shape domain over-approximates the may-point-to relation between the
set $\ptr^{lb}$ and the set of all symbolic addresses $\addr$. We define the
form of the heap template to be the formula

\begin{equation}
\templ^S \equiv \bigwedge_{\ssaplb{i} \in \ptrlb}
\templ^S_{\ssaplb{i}}(d_{\ssaplb{i}}).
\end{equation}

The template is a conjunction of template rows
$\templ^S_{\ssaplb{i}}$ where each row corresponds to a single loop-back
pointer $\ssaplb{i}$ and it describes the points-to relation of that pointer.
The parameter $d_{\ssaplb{i}} \subseteq \addr$ of the row (i.e., the
abstract value of the row) specifies the set of all addresses from the
set $\addr$ that $p$ may point to at the location $i$. The template row can be
therefore expressed as a disjunction of equalities between the loop-back
pointer and all possible addresses:

\begin{equation}
\templ^S_{\ssaplb{i}}(d_{\ssaplb{i}}) \equiv
(\bigvee_{a \in d_{\ssaplb{i}}} \ssaplb{i} = a)
\end{equation}

Computing an invariant in the given abstract domain allows 2LS to
characterize the shape of the program heap. For example, abstract values of
template rows corresponding to pointer fields of abstract dynamic objects
describe linked paths in the heap, such as linked segments.

§.§.§ Memory Safety Assertions

In order to analyse memory safety, 2LS automatically instruments the analysed
program by assertions to check for typical memory safety
errors [22, 23]. These are in particular pointer dereferencing
errors,  errors, and memory leaks.  We now describe the structure
of these assertions.

§.§.§ Dereferencing/Freeing a $\nullptr$ Pointer

To check for this kind of errors, 2LS adds an assertion $p \neq \nullptr$ to
each program location where $*p$ or  occurs. Since the shape
domain over-approximates the points-to relation, it is possible to soundly
prove absence of such errors. If an error is found, BMC can be used to check
whether it is spurious.

§.§.§ Dereferencing/Freeing a Freed Pointer

We introduce a special variable $\freevar$ initialised to $\nullptr$ that is
used to track the possibly freed objects. Every call to  in a
program location $i$ is replaced by a formula

\begin{equation}
\ssa{\freevar}{i} = \ssagfree{i} ? \ssa{p}{j} : \ssa{\freevar}{k}
\end{equation}

where $\ssa{p}{j}$ and $\ssa{\freevar}{k}$ are relevant versions of $p$ and
$\freevar$, respectively, valid at $i$, and $\ssagfree{i}$ is a free Boolean
variable. This formula represents a non-deterministic update of the value of
$\freevar$ by the freed address.

The shape domain is then used to over-approximate the set of all addresses that
$\freevar$ may point to, which is essentially the set of all possibly freed
memory objects. Proving  safety is then done by adding an
assertion $p \neq \freevar$ at each program location where $*p$ or

The nature of the shape domain guarantees soundness of this approach, however,
using it for abstract dynamic objects is often very imprecise. This is because
freeing one of the concrete objects represented by the abstract one does not
mean that the rest of the represented objects cannot be safely dereferenced or
freed. This problem is resolved by modifying the representation of
calls described in Section <ref>.

In addition to the set $\dynobjset{i}$ of abstract dynamic objects used to represent
all objects allocated at $i$, we add one object $\dynobj{i}{co}$ to
$\dynobjset{i}$. The object can be non-deterministically chosen as the
malloc result (just like any other $\dynobj{i}{k}$), however, it is guaranteed
to represent a concrete object (i.e., it can be allocated only once). This is
achieved by an additional condition asserting that $\dynobj{i}{co}$ cannot be
allocated if there is a pointer pointing to it at the entry to the allocation
site $i$. Therefore, the  representation has the form

\begin{equation}
p_i = (\ssagos{i, co} \wedge
\bigwedge_{p \in \ptr} p \neq \&\dynobj{i}{co} ) \,?\,
\&\dynobj{i}{co} :
(\ssagosij{i}{1} \,?\, \&\dynobj{i}{1} : (\dots))
\end{equation}

Afterwards, it is only allowed to assign the address of the concrete
object $\dynobj{i}{co}$ to $\freevar$ at each allocation site $i$. Checks for
the free safety are also done on concrete objects only, which helps to avoid
the described imprecision. This approach remains sound since $\dynobj{i}{co}$
represents an arbitrary object allocated at $i$ and if safety can be proven
for it, it can be assumed to hold for all objects allocated at $i$.

§.§.§ Memory Leaks Safety

Similarly to the previous section, the variable $\freevar$ is used to check for
safety from memory leaks. At the end of the program, we check whether there is
an object $\dynobj{i}{co}$ such that $\freevar \neq \&\dynobj{i}{co}$. If such
an object is found, a memory leak is present. However, proving absence from
memory leaks is only possible for loop-free programs (or for programs with all
loops fully unwound). This is because we do not track sequencing of abstract
objects representing concrete objects allocated at a single allocation site,
and our analysis typically sees that $\dynobj{i}{co}$ can be skipped in
deallocation loops, and hence remains inconclusive on the memory leaks.

§.§ Domain Combinations

One of the main advantages of program verification implemented in 2LS is that
all abstract domains are required to have a common form of
templates—quantifier-free first order formulae.  Thanks to this
feature, it is quite straightforward to create various compositions of
different domains while relying on the solver to do the heavy-lifting on the
domain operators combination and on mutual reduction of the domain abstract
values. In 2LS, we use two such combinations: product templates and
power templates, particularly their form called templates with
symbolic paths [22].

§.§.§ Product Templates

Product templates are one of the simplest forms of abstract domain combination
in 2LS. They are based on using a Cartesian product template that
combines domains of various kinds side-by-side. This can be achieved by simply
taking a conjunction of their templates.

A very interesting combination of this form is the combination of the shape and
polyhedra abstract domains. It allows 2LS to analyse values of variables of
pointer and numerical type at the same time. This helps not only for analysing
program manipulating pointers and numbers at the same time but also opens a
possibility to reason about contents of data structures at the program heap.
Thanks to this combination, it is possible to verify programs such as the one
in Figure <ref>.

§.§.§ Templates with Symbolic Paths

Using simple templates of invariants, such as the described polyhedra templates
or the heap shape template, may not be precise enough to analyse some programs,
especially programs working with abstract dynamic objects. In such programs, it
is often required that an invariant computed for a loop $l$ distinguishes which
loops were or were not executed before reaching $l$. When working with abstract
dynamic objects allocated in loops, this allows one to distinguish situations
when an abstract dynamic object does not represent any really allocated object,
and therefore an invariant describing it is not valid.

With respect to this, in order to improve precision, 2LS introduces the
concept of symbolic loop paths. A symbolic loop path expresses which
loops in the program were executed. Since 2LS uses loop-select guards to
capture the control flow through the loops, a symbolic path is simply a
conjunction of loop-select guard literals.

Formally, let $G^{ls}$ by the set of all loop-select guards in the analysed
program. A symbolic loop path $\pi$ is defined as

\begin{equation}
\pi = \bigwedge_{g \in G^{ls}} l_g
\end{equation}

where $l_g$ is a literal of $g$, i.e., $g$ or $\neg g$. We denote the set of
all symbolic paths by $\Pi$. We also define a special path $\pi_\perp$
containing negative literals only. For this path, no loop invariant is computed
since no loops were executed for this path.

Having some template $\templ$ expressing an abstract domain (e.g. the shape
domain or even a product domain), we define the corresponding template with
symbolic paths as

\begin{equation}
\templ^L \equiv \bigwedge_{\pi \in \Pi} \pi \implies \templ.
\end{equation}

This template can be viewed as a power template—in the sense of power
domains—which assigns to each element of the base domain an element of the
exponent domain.

The algorithm for inference of an invariant $\inv^L$ from a symbolic path
template is shown in Algorithm <ref>.

$\inv^L \gets \true$
$\pi \in \Pi$
add $\mathit{assert}(\pi)$ to solver
$\inv_\pi \gets $ compute invariant from $\templ$
remove $\text{assert}(\pi)$ from solver
$(\pi \wedge \inv_\pi)$ is satisfiable
$\inv^L \gets \inv^L \wedge (\pi \implies \inv_\pi)$

Algorithm for inferring an invariant from a symbolic paths template.

The algorithm computes a separate invariant $\inv_\pi$ in the inner domain
(using the template $\templ$) for each symbolic path $\pi$. To limit the
invariant computation for $\pi$ only, we assert that $\pi$ (a formula
expressing which loops are executed) holds during the computation. It may also
happen that, after computing $\inv_\pi$, the symbolic path is in fact not
reachable in the analysed program. Therefore, we check its reachability by
solving $\pi \wedge \inv_\pi$ in the context of the formula generated from the
SSA of the analysed program. If $\pi$ is reachable, then $\pi \implies
\inv_\pi$ is conjoined into the resulting invariant, otherwise $\inv_\pi$ is

§ IMPLEMENTATION AND ARCHITECTURE OF 2LS

2LS is based on the CPROVER framework.

2LS is implemented in C++ and currently has around 25 KLOC
(not counting CPROVER itself).

2LS does not have any external dependencies beyond CPROVER
and can therefore be built on many platforms.
However, it is currently well-tested under Linux only.

The source code is available at <https://www.github.com/diffblue/2ls>
under the BSD license.

2LS was initially developed by Daniel Kroening and
Peter Schrammel in 2014 and has received contributions
by more than 15 contributors since then.

2LS is compatible with most of CPROVER tools such
as , a drop-in replacement for GCC,
which can be used to build and link C source code using
the existing build system of the project to be analysed.
The resulting goto binary can be passed to 2LS
and other CPROVER tools for analysis, e.g. .

§.§.§ Architecture

Similarly to other verification tools, 2LS follows the pipeline architecture
of compilers, consisting of a front-end for parsing and
type checking the source code; middle-end passes for
transforming and optimising the code based on an intermediate
representation (typically in the single static assignment form, SSA);
and a back-end, which, however, instead of code generation
performs the analysis and verification.

An overview of the 2LS architecture is shown in Figure <ref>.

[line width=.5pt, >=latex]

boxnode = [rectangle, draw,minimum height=3em, minimum width=7em,
text width=6.5em, align=center, node distance=10em]
domainnode = [rectangle, draw, minimum height = 1.8em, minimum
width = 8.8em, node distance = 2.5em, align=center]

(src) at (0,0) source program;
[boxnode, right of = src] (goto) GOTO generator;
[boxnode, right of = goto] (analysis) Analysis + instrumentation;
[boxnode, right of = analysis] (ssa) SSA generator;

[boxnode, below of = src] (unwind) Unwinder;
[boxnode, below of = goto] (templ) Template generator;
[boxnode, below of = analysis] (inv) Invariant inference;

[domainnode, right = 2.1em of inv] (shape) Shape domain;
[domainnode, above of = shape] (interval) Interval domain;
[domainnode, below of = shape] (ranking) Ranking domain;
(ranking) – ($(ranking.south)+(0,-1.2)$) node [font=, midway, sloped] $\dots$;

[boxnode, below of = templ] (solver) SAT solver;
[boxnode, below of = inv] (prop) Property checker;
[boxnode, below = 2em of prop] (spurious) Spuriousness checker;

[->] (src) edge (goto);
[->] (goto) edge (analysis);
[->] (analysis) edge (ssa);
[->] (ssa) |- node [above, xshift = -10em] SSA ($(templ.north)+(0,1.3)$) – (templ);
[->] (templ) edge (inv);
[->] (inv) edge (prop);
[->] (prop) edge (spurious);
[->] (spurious) -| (unwind);
[->] (unwind) edge (templ);
[<->] (inv) edge (solver.north east);
[<->] (prop) edge (solver);
[<->] (spurious.north west) edge (solver.south east);
[<->] (interval.west) edge (inv.5);
[<->] (shape.west) edge (inv);
[<->] (ranking.west) edge (inv.-5);

[right = 4em of prop, yshift = 0.3em] (true)

[color=green!50!olive!80](0,.35) – (.25,0) – (1,.7) – (.25,.15) – cycle;

[right = 3.8em of spurious, yshift = 1.6em] (false)

[scale=2, red] 55;

[right = 4.5em of spurious, yshift = -1.6em, orange] (unknown)

[->] (prop.east) edge ($(prop.east)+(1.2,0)$);
[->] (spurious.east) edge ($(spurious.east)+(1.2,.35)$);
[->] (spurious.east) edge ($(spurious.east)+(1.2,-.35)$);

[right = 4em of ssa] (front) Front-End;
[below of = front, node distance = 11em] (middle) Middle-End;
[below of = middle, node distance = 12em] (back) Back-End;

2LS architecture overview.

§ EVALUATIONS

We now present results of the 2LS framework in the International Competition on
Software Verification (SV-COMP). 2LS has competed in SV-COMP since 2016. In the
first part, we compare the score that 2LS achieved over the years in chosen
categories that require the kinds of analyses that 2LS implements. In the
second part, we present some alternative rankings of the participating tools
that demonstrate strengths of 2LS other than just the amount of programs
successfully verified (e.g., time or power consumption).

§.§ Scores in SV-COMP

In this section, we show how the score obtained by 2LS in SV-COMP evolved over
the years (from 2016 to 2022). We highlight the important milestones that
caused a significant rise in the score and we also mention some of the tool's

Since SV-COMP consists of a large variety of verification tasks, we chose
several categories on which we demonstrate the tool's abilities.  We
concentrate on categories containing tasks whose verification requires program
analysis techniques that 2LS provides and that were described throughout this
chapter. In particular, we show the score in the following categories:

Loops + Floats Here, we give the sum of the scores obtained in the
Floats and the Loops sub-categories of the reachability
safety category

[In 2016, the SV-COMP categories layout was quite
different from the current one, however, the Floats and the
Loops categories already existed. Floats was a standalone
category, while Loops was a sub-category of
IntegersControlFlow. The presented results from 2016 show score
obtained in these (sub-)categories.].

Verification of programs in these categories requires inference of
invariants over numerical variables, which 2LS does using the template
polyhedra domain (Section <ref>). In particular, we always
used interval templates.

Heap One of the strengths of 2LS is analysis of heap-manipulating
programs. In SV-COMP, these are located in the ReachSafety-Heap
sub-category (where reachability of user-defined assertions is checked) and
in the MemSafety category (where tools verify absence of
memory-safety errors). This part gives the sum of these two
(sub-)categories. In order to analyse programs in this part, 2LS uses the
abstract shape domain described in Section <ref>.

Termination Besides verification of safety properties, 2LS allows to
verify termination of programs by employing both termination
(Section <ref>) and non-termination
(Section <ref>) analysis and running them in parallel.
In SV-COMP, termination is verified in the Termination category.

Overall The last kind of results that we show are those from the
Overall category that contains a (normalized) score obtained from
verification of all task programs in SV-COMP.

set layers
/pgf/number format/1000 sep=,
xmin=2016, xmax=2022,
ymin=-1500, ymax=8000,
legend style=at=(0.03,0.96),anchor=north west

(2016, 272)(2017, 393)(2018, 390)(2019, 861)(2020, 785)(2021, 1016)(2022, 1153)

Loops + Floats

(2017, -1288)(2018, 277)(2019, 270)(2020, 439)(2021, 1239)(2022, 947)

(2017, 624)(2018, 1522)(2019, 1279)(2020, 1264)(2021, 1315)(2022, 2178)

(2017, -1204)(2018, 4417)(2019, 4174)(2020, 4924)(2021, 6219)(2022, 7366)

Chosen results in SV-COMP 2016-2022

Figure <ref> shows the evolution of the score that 2LS
achieved in these categories between years 2016 and 2022 (in 2016, 2LS did not
compete in most of the categories). The most remarkable improvement can be seen
in 2018, where the score in the heap and the termination categories improved
heavily, which caused also an improvement of the overall score. The reason for
this is that in 2018, the abstract shape domain and the non-termination
analysis were added to 2LS.

Next, we select some achievements of 2LS in the mentioned categories, which
support claims about the framework's strengths:

* first place in Floats and second place in
Loops in 2016,

* third place in Termination in 2020, 2021, and 2022

* fourth place in Heap in 2019.

Last, one of the strengths of 2LS is the capability to reason about the shape
and content of unbounded dynamic data structures at the same time (thanks to
abstract domain combinations presented in Section <ref>). There
is no separate category for such programs; the only task programs requiring
such reasoning were added by our team in 2019 [22]. In 2022, 2LS
remains one of the only two tools that are capable to verify majority of these

§.§ Alternative Rankings

Besides the ability to soundly and correctly verify programs, there are other
properties that may support practical usefulness of a verification tool. In
this section, we compare 2LS to other verifiers using some alternative metrics,
in particular verification speed, energy consumption, and
correctness rate.

§.§.§ Speed of Verification in 2LS

One property that can be observed from the SV-COMP results is that 2LS verifies
most of the tasks in a very short time, compared to other tools. We support
this claim by an experiment where we set a small time limit and then observe
how 2LS would compete against other tools in SV-COMP'22.
Table <ref> shows the position that 2LS would achieve in some
of the main categories if the time limit was set to 5 seconds.

Position of 2LS in some SV-COMP'20 categories with a 5s time limit.

ReachSafety     MemSafety     NoOverflows     Termination     Overall

5.              5.            1.              1.              2.

The table shows that 2LS would achieve a high position in all of the mentioned
categories. A notable result is the first place in the Termination and
NoOverflows categories and the second place in the Overall

§.§.§ Power Consumption and Correctness Rate

In recent years, the competition report of SV-COMP [1] provides two
alternative rankings of verifiers that honor different aspects of the
verification process. These are in particular:

* Correct Verifiers which ranks the verifiers by a so-called
correctness rate, which is a ratio of the number of incorrect results
and the overall achieved score. 2LS finished third in this ranking in 2020
with only 0.0016 errors per score point[In SV-COMP, a tool is
granted 1 point for finding a bug in the program and 2 points for proving
the program safe. The final score is then computed by normalisation of the
scores obtained in the individual categories].

* Green Verifiers which ranks the verifiers by the amount of
energy used to achieve a single score point. In 2020 and 2021, 2LS finished
second in this ranking by using only 180 J per score point.

§.§ Evaluation Conclusion

Overall, we summarize the observations obtained from the SV-COMP results. 2LS
is able to prove true properties as well as to find counterexamples to property
violations. Most of the tasks that it is capable to prove, it proves very fast,
mainly thanks to the incremental unwinding of a single SAT instance.

However, 2LS does not scale to more complex problems. Reasons for this are
multiple: templates may be too weak, invariant inference does not scale to
complex templates, or k-induction often does not succeed.

Moreover, 2LS still lacks support for verification of a number of features of
programs, such as array contents, concurrency, or recursion. These prevent 2LS
from better positions in some categories (MemSafety, Overall).

§ CONCLUSIONS AND PROSPECTS

2LS is a verification system for C programs that is based on
a simple combination of bounded model checking, $k$-induction,
and template-based invariant inference.

The simplicity of the framework makes it easy to experiment
with new abstract domains.

2LS beats most other state-of-the-art tools in terms of
speed, but it still lagging behind in terms of robustness and
feature support.

For example, concurrency is not supported yet.

Also, recursion is not yet supported by its incremental
structural transformation algorithms.

Further improvements of the memory model will be required
to handle properties such as absence of memory leaks.

Invariant inference for arrays is another area of ongoing

[1]
Beyer, D.: Advances in automatic software verification: Sv-comp 2020.
In: A. Biere, D. Parker (eds.) Tools and Algorithms for the
Construction and Analysis of Systems, pp. 347–367. Springer (2020)

[2]
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without
In: Tools and Algorithms for the Construction and Analysis of
Systems, Lecture Notes in Computer Science, vol. 1579, pp. 193–207.
Springer (1999)

[3]
Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of
counterexamples to induction.
In: Formal Methods in Computer-Aided Design, pp. 173–180. IEEE
Computer Society (2007)

[4]
Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety Verification and
Refutation by $k$-Invariants and $k$-Induction.
In: Static Analysis Symposium, Lecture Notes in Computer
Science, vol. 9291, pp. 145–161. Springer (2015)

[5]
Brauer, J., King, A., Kriener, J.: Existential quantification as incremental
In: Computer-Aided Verification, Lecture Notes in Computer
Science, vol. 6806, pp. 191–207. Springer (2011)

[6]
Cabodi, G., Camurati, P., Mishchenko, A., Palena, M., Pasini, P.: SAT solver
management strategies in IC3: an experimental approach.
Formal Methods in System Design 50(1), 39–74 (2017).

[7]
Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-Precise
Procedure-Modular Termination Proofs.
TOPLAS 40 (2017)

[8]
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs.
In: Tools and Algorithms for the Construction and Analysis of
Systems, Lecture Notes in Computer Science, vol. 2988, pp. 168–176.
Springer (2004)

[9]
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction refinement.
In: Computer-Aided Verification, Lecture Notes in Computer
Science, vol. 1855, pp. 154–169. Springer (2000)

[10]
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for
static analysis of programs by construction or approximation of fixpoints.
In: Principles of Programming Languages, pp. 238–252 (1977)

[11]
D'Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning.
In: Principles of Programming Languages, pp. 143–154. ACM (2013)

[12]
Eén, N., Sörensson, N.: An Extensible SAT-solver.
In: SAT, Lecture Notes in Computer Science, vol. 2919, pp.
502–518. Springer (2003)

[13]
Eén, N., Sörensson, N.: Temporal induction by incremental SAT
Electronical Notes in Theoretical Computer Science 89:4,
543–560 (2003)

[14]
Gawlitza, T.M., Monniaux, D.: Improving strategies via SMT solving.
In: ESOP, Lecture Notes in Computer Science, vol. 6602, pp.
236–255. Springer (2011)

[15]
Gawlitza, T.M., Seidl, H.: Precise relational invariants through strategy
In: Computer Science Logic, Lecture Notes in Computer Science,
vol. 4646, pp. 23–40. Springer (2007)

[16]
Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint
In: Programming Language Design and Implementation, pp. 281–292. ACM

[17]
Günther, H., Weissenbacher, G.: Incremental bounded software model
In: SPIN, pp. 40–47. ACM (2014)

[18]
Hoder, K., Bjørner, N.: Generalized property directed reachability.
In: Theory and Applications of Satisfiability Testing, Lecture
Notes in Computer Science, vol. 7317, pp. 157–171. Springer (2012)

[19]
Hooker, J.N.: Solving the incremental satisfiability problem.
JLP 15(1&2), 177–186 (1993)

[20]
Kim, J., Whittemore, J., Sakallah, K.A., Silva, J.P.M.: On applying incremental
satisfiability to delay fault testing.
In: DATE, pp. 380–384. IEEE Computer Society (2000)

[21]
Madhukar, K., Schrammel, P., Srivas, M.K.: Compositional safety refutation
In: Automated Technology for Verification and Analysis, Lecture
Notes in Computer Science, vol. 10482, pp. 164–183. Springer (2017)

[22]
Malík, V., Hruška, M., Schrammel, P., Vojnar, T.: Template-based
verification of heap-manipulating programs.
In: FMCAD, pp. 103–111 (2018)

[23]
Malík, V., Hruška, M., Schrammel, P., Vojnar, T.: 2ls: Heap
analysis and memory safety (competition contribution)  (2019).

[24]
Malík, V., Martiček, Š., Schrammel, P., Srivas, M., Vojnar, T.,
Wahlang, J.: 2LS: Memory Safety and Non-termination (Competition
In: TACAS, pp. 417–421. Springer (2018)

[25]
Martiček, Š.: Synthesizing non-termination proofs from templates.
Master's thesis, Brno University of Technology, Brno (2017)

[26]
Marušák, M.: Generic template-based synthesis of program abstractions.
Master's thesis, Brno University of Technology, Brno (2019)

[27]
McMillan, K.L.: Lazy abstraction with interpolants.
In: Computer-Aided Verification, Lecture Notes in Computer
Science, vol. 4144, pp. 123–136. Springer (2006)

[28]
Miné, A.: The octagon abstract domain.
In: Working Conference on Reverse Engineering, pp. 310–319. IEEE
Computer Society (2001)

[29]
Monniaux, D., Schrammel, P.: Speeding up logico-numerical strategy iteration.
In: Static Analysis Symposium, Lecture Notes in Computer
Science, vol. 8723, pp. 253–267. Springer (2014)

[30]
Mukherjee, R., Schrammel, P., Haller, L., Kroening, D., Melham, T.: Lifting
CDCL to template-based abstract domains for program verification.
In: Automated Technology for Verification and Analysis, Lecture
Notes in Computer Science, vol. 10482, pp. 307–326. Springer (2017)

[31]
Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best
In: Verification, Model Checking, and Abstract Interpretation,
Lecture Notes in Computer Science, vol. 2937, pp. 252–266. Springer

[32]
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear
systems using mathematical programming.
In: Verification, Model Checking, and Abstract Interpretation,
Lecture Notes in Computer Science, vol. 3385, pp. 25–41. Springer

[33]
Schrammel, P.: Challenges in decomposing encodings of verification problems.
In: HCVS@ETAPS 2016, EPTCS, vol. 219, pp. 29–32 (2016)

[34]
Schrammel, P., Kroening, D.: 2LS for Program Analysis - (Competition
In: Tools and Algorithms for the Construction and Analysis of
Systems, Lecture Notes in Computer Science, vol. 9636, pp. 905–907.
Springer (2016)

[35]
Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T.,
Bienmüller, T.: Incremental bounded model checking for embedded
Formal Aspects of Computing 29(5), 911–931 (2017)

[36]
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using
induction and a SAT-solver.
In: FMCAD, Lecture Notes in Computer Science, vol. 1954, pp.
108–125. Springer (2000)

[37]
Silva, J.M., Sakallah, K.A.: Robust search algorithms for test pattern
In: FTCS, pp. 152–161. IEEE Computer Society (1997)

[38]
Strichman, O.: Pruning techniques for the SAT-based bounded model checking
In: CHARME, Lecture Notes in Computer Science, vol. 2144, pp.
58–70. Springer (2001)

[39]
Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: A new incremental
satisfiability engine.
In: DAC, pp. 542–545. ACM (2001)