Verifying Programs with Arrays and Lists

Julien Braine, Laure Gonnord, David Monniaux

► To cite this version:

Julien Braine, Laure Gonnord, David Monniaux. Verifying Programs with Arrays and Lists. [Internship report] ENS Lyon. 2016. hal-01337140

HAL Id: hal-01337140

https://hal.science/hal-01337140

Submitted on 24 Jun 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Verifying Programs with Arrays and Lists

Julien BRAINE

M2's internship with Laure Gonnord and David Monniaux. February-June 2016

Abstract

Automatically verifying safety properties of programs is a tough problem that has been tackled using many different approaches: rewriting systems, abstract interpretation, SMT solving, ...

Most techniques restrict themselves to programs operating on boolean and integer values and transposing them to infinite data structures such as arrays has not yet been satisfyingly achieved.

Recent work in Monniaux and Gonnord [2016] suggests the use of abstract interpretation to transpose programs containing arrays into Horn clauses that do not contain arrays. The major innovation of their work is that they use Horn clauses which are more general than programs, to obtain better results.

In this work, we first set the work of Monniaux and Gonnord in a more general framework that allows us to extend their abstractions, simplify the expressions they generate, and analyze the precision of their abstraction.

Finally we extend their abstractions so that we can analyze lists and experiments show that we succeed to analyze several classical examples, including sorting algorithms.

Contents

<table><tr><td>1</td><td>Introduction</td><td>1</td></tr><tr><td>2</td><td>From programs to Horn problems</td><td>2</td></tr><tr><td>3</td><td>To language independent Horn problems</td><td>3</td></tr><tr><td>3.1</td><td>Conversions: definition and issues</td><td>3</td></tr><tr><td>3.2</td><td>Conversions to a language independent theory</td><td>3</td></tr><tr><td>4</td><td>Constructing formal conversions</td><td>6</td></tr><tr><td>4.1</td><td>Abstractions</td><td>6</td></tr><tr><td>4.2</td><td>New approach: a step by step conversion of Horn clauses</td><td>7</td></tr><tr><td>5</td><td>To the theory of Horn solvers</td><td>12</td></tr><tr><td>5.1</td><td>Related work: array abstraction</td><td>12</td></tr><tr><td>5.2</td><td>Contributions: new abstractions</td><td>15</td></tr><tr><td>6</td><td>Implementation and experiments</td><td>18</td></tr><tr><td>7</td><td>Conclusion and perspectives</td><td>19</td></tr></table>
# 1 Introduction

Avoiding bugs when writing programs has always been tough for many reasons: programmers must think, for example, about integer overflows, unpredicted user input and memory management. Several methods exist to avoid bugs: good coding habits and proper documentation but only automated error checking can prove their absence.

The latter requires us to define what an error is. There are errors defined by the programming language such as out of bound array accesses, and there are errors due to the semantics of the program. The former errors can be directly checked, however, the latter requires the user to add specifications. In Example 1, the user adds specifications in the form of assertions ensuring the semantics and then the bug checking tool can add automatic assertions due to well-known errors.

<figure><img src="image_2.png" /><figcaption>**Example 1 (Array Initialization in C++)**</figcaption></figure>

Once specifications have been given, there are several ways to detect bugs:

* The simplest technique consists in modifying the program such that, during its execution, when an assertion fails, its saves an execution trace and files an error report so that the bug can be removed. Although the end-user experiences the bug, this method is a good solution for programs that do not have high security or quality of service requirements.

* Another technique consists in running tests on the program, hoping that they will catch most bugs. The end user does not experience any issues when a bug is caught with this technique, but there is no guarantee that all bugs are caught.

* The technique we will be focusing on this work, called static analysis, does not suffer from those flaws: we run the program symbolically, covering all possible execution traces and checking that no assertion fails. The main issue is that there exists no program that can check that no possible execution fails: the problem is undecidable. Static analysis is most suited for high security programs such as in avionics and programmers might have to help the analyzer.

During the life cycle of a given software, a combination of these techniques is usually used, weighted by time development and security requirements: these techniques serve different purposes.

Static analysis is mainly used to ensure that there are no bugs in a program whereas other techniques are used to detect bugs within programs. In this work, we focus on the design of static analyzers that over-approximate the behaviors of programs, and prove their safety. They will either return that there is no bug in a program, or “don’t know”.

Within the perimeter of this work are two categories of techniques to analyze programs:

* Abstract interpretation (Cousot and Cousot [1977]) consists in abstracting (possibly infinite) sets of possible values by an abstract object (for instance intervals, polyhedra, ...) and map
operations on programs to operations on the abstract object. The analysis then returns that there is a possible error when one of the values of the abstract object makes an assertion fail. The Astree tool (Cousot et al. [2005]) has successfully applied this technique to analyze many industrial size critical programs.

* Logic based solving consists in writing (an approximation of) the semantics of a program as a logic formula that is then solved by a SAT Modulo Theory solver(SMT) such as Z3¹, Z3-Spacer<fnref n="2" /> and Eldarica<fnref n="3" />.

These techniques have been extensively studied on programs containing bounded data (or numeric data) but have not been able to successfully analyze programs using unbounded data structures such as arrays, lists, trees or graphs. Building on Monniaux and Gonnord [2016], we convert analyses on unbounded data structures to analyses on bounded structures.

**Technique** We use abstract interpretation to convert logic formulas, called Horn problems, on unbounded data structures into Horn problems on bounded data structures, that can then be solved by state-of-the-art SMT solvers.

**Contribution** The contributions of this work are:

* A framework for abstract interpretation on Horn clauses. This framework is used to increase the generality of current abstractions, to construct new abstractions and simplify proofs.

* An explicit abstract interpretation for linear data structures such as lists.

* An implementation that succeeds to prove the correctness of some sorting algorithms.

**Organization of report** In Section 2, we convert programs into logic formulas called Horn clauses. Then, Section 3 explains the conversion of these Horn clauses into a common base language. In Section 4 we give the framework for abstract interpretation on Horn clauses, then used in Section 5 to give abstractions that convert Horn clauses on unbounded data into Horn clauses over bounded data. Finally, in Section 6, we describe our implementation and give the experimental results.

## 2 From programs to Horn problems

A Horn problem is a special subset of first order formula that can capture the semantics of a program. A Horn problem over a theory $\mathcal{T}$ is a formula that can be written in the following form.

$$ \exists P_1, \dots, P_n, \bigwedge_i \forall v_{i_1}, \dots, v_{i_k} C_i $$

where:

* $P_1, \dots, P_n$ are existentially quantified functions, called predicates, from types of $\mathcal{T}$ to $\mathit{Bool}$.

* $v_{i_1}, \dots, v_{i_k}$ are variables with types in $\mathcal{T}$

* $C_i$ is a clause in the form $cond_1 \wedge cond_2 \wedge \dots \wedge cond_j \Rightarrow result$ and each condition and the result is either a predicate applied to variables or a formula in the theory of $\mathcal{T}$.

The simplest way to visualize Horn problems is through programs. A program can be transformed into a Horn problem that captures its semantics, that is to say into a Horn problem that is unsatisfiable if and only if there is an execution of the program such that an assertion fails. A possible

<footnote n="1">¹https://github.com/Z3Prover</footnote>

<footnote n="2">²https://bitbucket.org/spacer/code</footnote>

<footnote n="3">³https://github.com/uuverifiers/eldarica/</footnote>
transformation consists in three steps:

1. Retrieve the control flow graph(CFG) of the program, on Example 1 this gives Example 1.1.

2. Interpret a state of the CFG as a predicate indicating the possible variable values at that state.

3. Interpret each edge $e$ of the CFG as a relation $R$ between the values at the source of $e$ and the target of $e$, creating the clause: $\forall vars, vars', Source vars) \wedge R Communication vars, vars') \Rightarrow End Communication vars')$.

We give the result of this transformation applied to Example 1 in Example 1.2. As such, the Horn problem in Example 1.2 can not be run on a SMT solver: SMT solvers do not deal with the theory of a programming language. In the next sections, we convert Horn problems generated by the conversion from a CFG, to Horn problems that can be run on a SMT solver.

# 3 To language independent Horn problems

In practice, Horn solvers do not run on theories that express all program operations. The basic theory, we call *Basic*, on which Horn solvers run simply have types `Int = Z`, `Real = R`, `Bool = {0, 1}` and tuple types (that is to say pairs, triples, ...) with usual arithmetical operations<fnref n="4" />.

In this section, we convert Horn problems to a language independent theory that will be converted to the *Basic* theory later on.

## 3.1 Conversions: definition and issues

**Definition 3.1** A Horn problem conversion from a source theory to a target theory is a function that to a Horn problem over the source theory associates a Horn problem over the target theory.

For a conversion `conv` to be useful, we require two properties:

* Soundness: $conv(H)$ satisfiable $\Rightarrow H$ satisfiable. Ensures that when an analysis returns that there are no bugs, then there are no bugs in the original program.

* Precision: $H$ satisfiable $\Leftrightarrow conv(H)$ satisfiable. Ensures the relevance of checking for a bug when an analysis returns that there is potentially a bug.

In the rest of this section, we do not simplify the theories on which Horn problems are, we only convert them to a language independent theory without any loss of precision: we use conversions called *complete*, that is to say conversions $c$ such that $\forall H, c(H) \Leftrightarrow H$.

## 3.2 Conversions to a language independent theory

The goal of this section is to convert a Horn problem over a theory of a programming language into a Horn problem over a language independent theory we call *Fundamental*, containing the *Basic* theory and language independent unbounded data structures. However, doing so is a full research topic on its own<fnref n="5" /> and we focus on giving the intuition of the conversions involved, the main contribution of this document starting once we have reached *Fundamental*. Example 1.3 illustrates the expected result of this section on Example 1.2.

<footnote n="4">⁴The *Basic* theory is the theory well dealt by all solvers, though many solvers have extensions.</footnote>

<footnote n="5">⁵Some tools such as SEAHORN https://seahorn.github.io/ and FramaC http://frama-c.com/ provide support for developing such abstractions.</footnote>
<figure><img src="image_3.png" /><figcaption>**Example 1.2** (Automated Basic Horn problem associated to CFG of Example 1.1)</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>**Example 1.3** (Complete conversion from array to Function of Horn problem of Example 1.2)</figcaption></figure>

We use simplified notation: quantifiers are assumed.

<figure><img src="image_5.png" /></figure>
### 3.2.1 Converting non pointer types: bool, int, floats and primitive structures

**bool conversion** The conversion for *bool* is very simple as the Horn basic theory has the *Bool* type which is exactly equivalent, therefore, there is nothing to do.

**int conversion** *int* in most programming languages is bound, therefore there is no exact equivalent type in the basic Horn theory<fnref n="6" />: the *Int* Horn type is infinite. We convert *int* to *Int* and do each operation modulus *INT_MAX*.

**float conversion** The Horn basic theory<fnref n="7" /> does not have floating point numbers but contains reals. The Real type is suited for specifications that do not depend on rounding errors, but general specifications require another approach: use an exponent and a mantissa integer, and convert the operations on floating point numbers to operations on the couple (exponent, mantissa).<fnref n="8" />

**primitive structures** Primitive structures are equivalent to the tuple of their elements. We abstract a primitive structure into the tuple of its abstracted elements.

### 3.2.2 Converting unbounded structured data types: arrays, lists, trees, graphs

In most programs data types are bounded either by the available memory or some big number such as *INT_MAX*. However, abstracting data types bounded by such numbers by the tuple of its elements does not give an effective solution for performance reasons.

**array<T> conversion** We introduce the mathematical type *FunctionITIVE*, *T* in the *Fundamental* theory<fnref n="9" /> and consider that an array is just a function and a size. We define two operations on *FunctionITIVE*, *T* to mimic the *access* and *write* operations on *array<T>*:

* `select(f, index)` which returns `f(index)`.

* `store(f, index, value)` which returns a function `g` identical to `f` except that `g(index) = value`.

Converting arrays to functions then consists in replacing:

* `a ∈ array<T>` by `(size, f) ∈ int × FunctionITIVE`, *T*

* `access(a, i)` by `(size, select(f, i))`

* `write(a, i, v)` by `(size, store(f, i, v))`

* `size(a)` by `size`

This conversion applied to Example 1.2 gives the Horn problem in Example 1.3.

**list<T> conversion** Lists are almost semantically equivalent to arrays: they describe a linear data structure and the main difference is not in the semantics, but in the implementation which gives different operation complexity. The only operations that are semantically specific to lists are the *insert* and *erase* operations, and we need to introduce the equivalent operations on functions within the *Fundamental* theory.

**Trees, DAGs, Graphs, ... conversions** Concerning trees and graphs or even other unbounded data structures such as DAGs, we keep the same idea: expand the *Fundamental* theory with the underlying infinite data structure and its operations and manage the finite aspect by adding size

<footnote n="6">⁶Some solvers have bit-vectors that can be used for bounded integers.</footnote>

<footnote n="7">⁷Some solvers can deal with floating point arithmetic.</footnote>

<footnote n="8">⁸This conversion is naive and causes solving time issues. Finding a good conversion is a full research topic.</footnote>

<footnote n="9">⁹This has already been done in some solvers.</footnote>
integers. In the case of trees for example, one would want to enlarge the theory with infinite depth and width trees and the operations insert, erase, select and store on those trees.

### 3.2.3 Pointers

We do not deal with unstructured data in this work. However, in many cases pointers are the implementation of semantically structured data dealt within this work. Some cases have solutions: argument passing as pointers (or references) can be dealt with the copy and return idiom, pointers allocated with malloc have the semantics of array, ... Other cases, such as retrieving lists and trees represented by pointers, can be handled using shape analysis (Jones and Muchnick [1982]) and separation logic (Reynolds [2002]) for example. These concerns are not tackled in this work and can be researched upon and dealt with independently.

## 4 Constructing formal conversions

In the previous section we gave informal examples of conversions and although the abstractions behind those conversions are fairly intuitive, properly defining these conversions can be difficult. The goal of this section is to construct conversions from abstractions.

### 4.1 Abstractions

A general abstraction from a variable of type *Source* to a type *Target* is a Galois connection $\mathcal{G}: \mathcal{P}(\mathcal{Source}) \overset{\gamma}{\underset{\alpha}{\rightleftarrows}} \mathcal{P}(\mathcal{Target})$ and a set of abstract operations (Cousot and Cousot [1977]). Intuitively $\mathcal{G}$ formalizes how states of the CFG representing possible values of *Source* now represent possible values of *Target*. The abstract operations then correspond to defining the edges of the CFG as a relationship between values of *Target* instead of values of *Source*.

In this work, we do not abstract sets of possible values of *Source* by single values of *Target* as done in polyhedral abstract interpretation Cousot and Halbwachs [1978]: simplifying sets of possible values is dealt by the SMT solver during predicate calculation. Instead, we abstract single values of complex types into possibly multiple values of simple types: we use one to many abstractions and the informal array to function conversion of Section 3.2.2 is defined in Abstraction 1.

**Definition 4.1** Let $\phi$ be a function from $\mathcal{Source} \to \mathcal{P}(\mathcal{Target})$. $\phi$ induces a Galois connection $\mathcal{G}: \mathcal{P}(\mathcal{Source}) \overset{\gamma}{\underset{\alpha}{\rightleftarrows}} \mathcal{P}(\mathcal{Target})$ called one to many abstraction associated to $\phi$ defined by:

$$ \left\{ \begin{array}{l} \alpha(\mathit{concrete} \in \mathcal{P}(\mathit{Source})) = \bigcup_{c \in \mathit{concrete}} \phi(c) \\ \gamma(\mathit{abstracted} \in \mathcal{P}(\mathit{Target})) = \{c \in \mathit{Source}, \phi(c) \subseteq \mathit{abstracted}\} \end{array} \right. $$

<table><caption>**Abstraction 1** (One to many Galois connection for array to function conversion)</caption><thead><tr><th>$\phi(a \in \mathit{array}\langle\mathit{int}\rangle) = \{\mathbf{size}, \mathbf{f}\}, \mathit{size} = \mathit{size}(a), \forall i \in [0, \mathit{size}(a)][, \mathit{f}(i) = a[i]\}$</th><th></th></tr></thead><tbody><tr><td><i>Concrete operation</i></td><td><i>Abstract operation</i></td></tr><tr><td>$\mathit{access}(a, i)$</td><td>$(\mathbf{size}, \mathit{select}(\mathbf{f}, i))$</td></tr><tr><td>$\mathit{write}(a, i, v)$</td><td>$(\mathbf{size}, \mathit{store}(\mathbf{f}, i, v))$</td></tr><tr><td>$\mathit{size}(a)$</td><td>$\mathbf{size}$</td></tr></tbody></table>

A common method replaces each operation $c_{op}(vars)$ by an operation $a_{op}(vars^#)$, $vars^#$ representing an abstraction of *vars*, as has been done in Abstraction 1. In many cases described in Section 5.1, there is no precise enough abstract operation and most papers suggest abstracting edges of
the form $P_1(\mathit{vars}) \wedge \mathit{vars}' = c_{\mathit{op}}(\mathit{vars}) \Rightarrow P_2(\mathit{vars}')$ instead of operations. This approach creates several unwanted consequences:

* Horn problems that have several predicates in their clauses conditions can not be transformed into clauses of the form $P_1(\mathit{vars}) \wedge \mathit{vars}' = c_{\mathit{op}}(\mathit{vars}) \Rightarrow P_2(\mathit{vars}')$. Although this is not an issue for Horn problems directly induced by programs, we can no longer compose conversions that take advantage of several predicates in the clause's conditions.

* The performance might be impacted when Horn problems are transformed, as edges with multiple composed operations such as $\mathit{var} = \mathit{read}(\mathit{store}(a, i, v), j)$ must be separated into several edges, adding temporary variables and predicates.

Furthermore, when a clause of the form $P_1(\mathit{vars}) \wedge \mathit{vars}' = c_{\mathit{op}}(\mathit{vars}) \Rightarrow P_2(\mathit{vars}')$, representing an edge is abstracted by a clause such as $P_1^{\#}(\mathit{vars}_1^{\#}) \wedge P_1^{\#}(\mathit{vars}_2^{\#}) \Rightarrow P_2^{\#}(\mathit{vars}'^{\#})$, as has been done in Monniaux and Gonnord [2016], several problem arise:

* The semantics of the abstractions are harder to grasp as an edge is abstracted into a clause that is not an edge, thus proving soundness is much harder.

* Local abstraction, operation abstraction on clause level quantified parameters, and global abstraction, the abstractions of predicates that are quantified at the top level, are mixed up. Understanding whether the precision loss is due to operation abstraction or $\phi$ is thus harder.

* Modularity is impacted: what if we only wish to abstract only some operations or predicates ?

The major contributions of this section are:

* An approach in which abstractions can be defined that does not suffer from the above issues.

* An explicit algorithm for conversions induced by abstractions.

## 4.2 New approach: a step by step conversion of Horn clauses

Our approach is defined for one to many abstractions $\phi$. The key idea is to make an explicit use of $\phi$, allowing us to separate the abstractions of predicates from the abstractions of operations. The major steps of the conversion are given through the pseudo-code given in Algorithm Convert[1], and will be developed later on.

**Algorithm 1: Convert[1]:** Conversion induced by abstraction algorithm

Input: HornProblem $H$, Variable $v$, $Expr \to Expr AbsExpr$
foreach Clause $C \in H$ do AbsOp[2]($C$, AbsExpr, $v$); // $v$ in each clause is limited to $\phi(v)$
foreach Predicate $P \in H$ do AddAbsPredicate[3]($P$); // Abstract predicates $P^\#$ created
foreach Clause $C \in H$ do UseAbsPredicate[4]($C$); // $P$ and $\phi$ within clause's removed
Finalize[5](); // The Horn problem is over the target theory

We illustrate the new approach through Example 2 on which we execute each major step of the Algorithm Convert[1] with Abstraction 1 as parameter.

<table><caption>**Example 2 (Example on which we demonstrate the new approach)**</caption><thead><tr><th>Functionality</th><th colspan="2">Increments cell i of an array a and checks that it has been incremented</th></tr></thead><tbody><tr><th scope="row">Types</th><td colspan="2">((i, j, a), (i', j', a')) ∈ (int × int × array&lt;int&gt;)<sup>2</sup></td></tr><tr><th scope="row">Start ⇒ false</th><td colspan="2">i ≥ size(a)</td></tr><tr><th scope="row">Start ⇒ Increase</th><td colspan="2">i < size(a) ∧ i' = i ∧ j' = read(a, i) ∧ a' = a</td></tr><tr><th scope="row">Increase ⇒ Check</th><td colspan="2">i' = i ∧ j' = j ∧ a' = write(a, i, read(a, i) + 1)</td></tr><tr><th scope="row">Check ⇒ false</th><td colspan="2">j + 1 ≠ read(a, i)</td></tr></tbody></table>
### 4.2.1 AbsOp[2] procedure

To improve expressiveness of operation abstraction, we abstract expressions of the form `tmp = c_{op}(args)` instead of operations `c_{op}(args)`, giving us the added expressiveness of relations. Although the idea is similar to abstracting a whole edge `P_1 vars ∧ vars' = c_{op}(vars) ⇒ P_2 (vars')`, there are two main differences in our abstract expressions:

* We only abstract `tmp = c_{op}(args)` and not an edge, that is to say that the abstract expression must only involve `tmp` and `args`.

* We explicitly use `φ` in the abstractions as shown in Example 2.1, allowing us to keep the concrete predicates and abstract them later on.

We do not involve predicates in the transformation and we avoid the many disadvantages described in Section 4.1 of directly abstracting edges. The expressiveness of abstracting expressions in such a way is equivalent to the expressiveness of edge abstraction<fnref n="10" /> and the main issue is finding a way to abstract predicates and remove the uses of `φ`. The formal abstract expressions induced by Abstraction 1 are given in Example 2.1.

<table><caption>**Example 2.1 (Abstract expressions of array to function conversion)**</caption><thead><tr><th>Concrete expression</th><th>Abstract expression</th></tr></thead><tbody><tr><td>var = write(a, i, v)</td><td>∃(var<sub>size</sub>, var<sub>f</sub>), (a<sub>size</sub>, a<sub>f</sub>), ∧ { (var<sub>size</sub>, var<sub>f</sub>) ∈ φ(var) ∧ (a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a) (var<sub>size</sub>, var<sub>f</sub>) = (a<sub>size</sub>, store(a<sub>f</sub>, i, v))</td></tr><tr><td>var = read(a, i)</td><td>∃(a<sub>size</sub>, a<sub>f</sub>), (a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a) ∧ var = select(a<sub>f</sub>, i)</td></tr><tr><td>var = size(a)</td><td>∃(a<sub>size</sub>, a<sub>f</sub>), (a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a) ∧ var = a<sub>size</sub></td></tr></tbody></table>

The main idea in Algorithm AbsOp[2] is to **Replace** any expression of the form `tmp = c_{op}(args)` by its abstract expression. To do so, we first need to **Normalize** the clause to decompose expressions into several expressions of the form `tmp = c_{op}(args)` and **Rearrange** the clause into standard form after having replaced the expressions. In fact, this last step requires that the only quantifiers within the abstract expressions are existential quantifiers placed at the beginning <fnref n="11" />. Furthermore, in order for Algorithm Convert[1] to succeed, we require that expressions of the form `var# ∈ φ(var)` only appear positively in abstract expressions, but we have not met cases where this is an issue.

**Algorithm 2: AbsOp[2]: abstracting expressions**

Input: Clause C, *Expr* → *Expr* AbsExpr
Normalize(C); // All expressions are either predicates or tmp = c_{op}(args)
foreach Expression e ∈ C do Replace(e, AbsExpr(e)); // All expressions are abstracted
Rearrange(C); // The clause is in Horn standard format

Each step of Algorithm AbsOp[2] applied on Clause 3 is given in Example 2.2.

**Soundness and precision analysis** The normalization and the rearranging steps are complete conversions, therefore the soundness and the precision of the global conversion are equivalent to the soundness and completeness of the replace conversion. The replace conversion is sound (resp. complete) if and only if the abstract expression implies (resp. is equivalent to) the concrete expression.

<footnote n="10">¹⁰We can generate any Horn problem that was generated through edge conversion after all the steps of the conversion.</footnote>

<footnote n="11">¹¹This ensures that the problem remains a Horn problem.</footnote>
<table><caption>**Example 2.2** (Steps of Algorithm AbsOp[2] on Clause 3)</caption><thead><tr><th>Edge</th><th>Increase ⇒ Check</th></tr></thead><tbody><tr><td>Input</td><td>i' = i ∧ j' = j ∧ a' = write(a, i, read(a, i) + 1)</td></tr><tr><td>Normalized</td><td>i' = i ∧ j' = j ∧ tmp1 = read(a, i) ∧ tmp2 = tmp1 + 1 ∧ a' = write(a, i, tmp2)</td></tr><tr><td>Replaced</td><td>∧ <span style="font-size: 2em; vertical-align: middle;">{</span> <div style="display: inline-block; vertical-align: middle; text-align: left; line-height: 1.2em;"><span style="display: block; border-bottom: 1px solid black; padding: 0 0.2em;">i' = i ∧ j' = j ∧ tmp2 = tmp1 + 1</span><span style="display: block; padding: 0 0.2em;">∃(a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a), tmp1 = select(a<sub>f</sub>, i)</span><span style="display: block; padding: 0 0.2em;">∃(a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a), (a'<sub>size</sub>, a'<sub>f</sub>) ∈ φ(a'), (a'<sub>size</sub>, a'<sub>f</sub>) = (a<sub>size</sub>, store(a<sub>f</sub>, i, tmp2))</span></div></td></tr><tr><td>Rearranged</td><td>∧ <span style="font-size: 2em; vertical-align: middle;">{</span> <div style="display: inline-block; vertical-align: middle; text-align: left; line-height: 1.2em;"><span style="display: block; border-bottom: 1px solid black; padding: 0 0.2em;">(a<sub>size</sub>, a<sub>f</sub>) ∈ φ(a) ∧ (a'<sub>size</sub>, a'<sub>f</sub>) ∈ φ(a') ∧ i' = i ∧ tmp2 = tmp1 + 1</span><span style="display: block; padding: 0 0.2em;">j' = j ∧ tmp1 = select(a<sub>f</sub>, i) ∧ (a'<sub>size</sub>, a'<sub>f</sub>) = (a<sub>size</sub>, store(a<sub>f</sub>, i, tmp2))</span></div> (Clause 5)</td></tr></tbody></table>

### 4.2.2 AddAbsPredicate[3] procedure

Predicates are the existentially quantified functions expressing the set of possible values at a program state, when using Horn clauses induced by programs. When using an abstraction, we abstract a concrete predicate representing a set of possible concrete values $S_1$ at a program state by predicate representing a set of possible abstract values $S_2 = \alpha(S_1) = \bigcup_{v \in S_1} \phi(v)$.

For a predicate $P$, we CreatePredicate an abstract predicate $P^#$ such that (1) expressing that $P^#$ is an abstraction of $P$ is verified.

$$ \forall \text{args}, v, (v^# \in \phi(v) \Rightarrow (P^#(\text{args}, v^#) \Leftrightarrow P(\text{args}, v))) \quad (1) $$

In fact, (1) can be rewritten as a conjunction of two clauses that we AddClause directly in the Horn problem giving the Algorithm AddAbsPredicate[3].

**Algorithm 3: AddAbsPredicate[3]:** adding abstract predicates

Input: Predicate $P$, HornProblem $H$, Type AbstractType
CreatePredicate($H, P^#, AbstractType$); // Predicate $P^#$ created
Let $C_{P_\alpha} = \forall arg, v, v^#, v^# \in \phi(v) \land P(arg, v) \Rightarrow P^#(arg, v^#)$; // Condition forcing $\alpha(P) \subseteq P^#$
Let $C_{P_\gamma} = \forall arg, v, v^#, v^# \in \phi(v) \land P^#(arg, v^#) \Rightarrow P(arg, v)$; // Condition forcing $P \supseteq \gamma(P^#)$
AddClause($H, C_{P_\alpha}$) AddClause($H, C_{P_\gamma}$)

Applying AddAbsPredicate[3] on the Increase predicate of Example 2 gives Example 2.3.

<table><caption>**Example 2.3** (Added clauses by AddAbsPredicate[3] on Increase of Example 2)</caption><tr><td>Clause $C_{Increase_\alpha}$: ($a_{size}, a_f$) ∈ $\phi(a) \land Increase(i, j, a) \Rightarrow Increase^#(i, j, a_{size}, a_f)$</td></tr><tr><td>Clause $C_{Increase_\gamma}$: ($a_{size}, a_f$) ∈ $\phi(a) \land Increase^#(i, j, a_{size}, a_f) \Rightarrow Increase(i, j, a)$</td></tr></table>

**Soundness and precision analysis** The conversion is sound as the original problem is contained within the new problem. The conversion is complete if and only if $\gamma \circ \alpha = \text{Id}$. In practice, we only lose precision if $P$ is a solution to the original problem and $\gamma(\alpha(P))$ is not.

### 4.2.3 UseAbsPredicate[4] procedure

Once abstract predicates have been added, the goal is to replace concrete predicates by abstract predicates, first in the result of each clause, then in the conditions of each clause. The first step consists in using (1) to define the complete conversion: Replace, in the result of a clause, $P(args, v)$ by $P^#(args, v^#)$ when $v^# \in \phi(v)$ is in the conditions.
The second step follows the same idea and the first attempt for the second step conversion gives: replace, in the condition of a clause, $P(args, v) \wedge v^{\#} \in \phi(v)$ by $P^{\#}(args, v^{\#})$. We extend the idea for any number of predicates and uses of $\phi$. For $n$ predicates and $k$ uses of $\phi$, the conversion consists in replacing (2) by (3).

$$ \left( \bigwedge_{i \in [0,n]} P_i(args_i, v) \right) \wedge \left( \bigwedge_{j \in [0,k]} v_k^{\#} \in \phi(v) \right) \quad (2) \qquad \bigwedge_{i \in [1,n], j \in [0,k]} P_i^{\#}(args_i, v_j^{\#}) \quad (3) $$

Although this conversion is sound, it is not complete: we do not have (2) $\Leftrightarrow$ (3). In fact, we have (2) $\Leftrightarrow$ ((3) $\wedge$ AreAbstractions$_k(v_1^{\#}, \dots, v_k^{\#})$) with AreAbstractions$_k(v_1^{\#}, \dots, v_k^{\#})$) equivalent to (4)

$$ \exists v, \forall j \in [0, k], v_j^{\#} \in \phi(v) \quad (4) $$

Therefore, the second step conversion consists in replacing (2) by (3) $\wedge$ AreAbstractions$_k(v_1^{\#}, \dots, v_k^{\#})$. We combine the first and second step, we get Algorithm UseAbsPredicate [4].

<caption>**Algorithm 4: UseAbsPredicate [4]:** replacing concrete predicates by abstract predicates</caption>

**Input:** Clause C, Int($k$) $\rightarrow$ (Variable$^k$) $\rightarrow$ Expr AreAbstractions
**Let** $\forall$ params, conditions(args) $\wedge$ $v^{\#} \in \phi(v) \Rightarrow P(args, v) = C$; // Decomposition of C
**Replace** (C, $\forall$ params, conditions(args) $\wedge$ $v^{\#} \in \phi(v) \Rightarrow P^{\#}(args, v^{\#})$); // First step done
**foreach** Predicate $P_i$ such that $P(args_i, v) \in C$ **do**
| **foreach** Variable $v_j^{\#}$ such that ($v_j^{\#} \in \phi(v)$) $\in C$ **do** AddCondition(C, $P_i^{\#}(args_i, v_j^{\#})$);
| RemoveCondition(C, $P_i(args_i, v)$); // $P_i(args_i, v)$ replaced by $\wedge_j P_i^{\#}(args_i, v_j^{\#})$
**end** // All $P_i$ are abstracted
**Replace**($v_1^{\#} \in \phi(v) \wedge \dots \wedge v_k^{\#} \in \phi(v)$, AreAbstraction($v_1^{\#}, \dots, v_k^{\#}$)); // $\phi$'s removed

However, if AreAbstractions is written as in (4), we introduce a concrete variable as well as many uses of $\phi$. We wish to write AreAbstractions without using any concrete variables. In all the abstractions we have seen so far, we have been able to define AreAbstractions$_k$ for any needed $k$ without using any other variables than $v_1^{\#}, \dots, v_k^{\#}$. To give some insight of how simple AreAbstractions can be, we give AreAbstractions in Example 2.4 for Abstraction 1.

<table><caption>**Example 2.4 (AreAbstractions for array to function conversion)**</caption><tr><td>AreAbstractions<sub>1</sub>(size, f)</td><td>size ≥ 0</td></tr><tr><td>AreAbstractions<sub>k</sub>((size<sub>1</sub>, f<sub>1</sub>), ..., (size<sub>k</sub>, f<sub>k</sub>))</td><td>\bigwedge_{j \in [1,k]} size<sub>j</sub> ≥ 0 \wedge \forall i, f<sub>1</sub>(i) = f<sub>2</sub>(i) = \dots = f<sub>k</sub>(i)</td></tr></table>

*Remark: for $k > 1$, AreAbstractions$_k$ is not a valid Horn condition. Fortunately, there is no need for $k > 1$ with the abstract expressions defined in Example 2.1 as they use at most one existentially quantified abstraction of a given concrete variable.*

We apply UseAbsPredicate [4] on Clause 5 of Example 2.2 to get Example 2.5.

**Soundness and precision analysis** The conversion is sound (respectively complete) if and only if (1) is implied by the Horn problem and AreAbstraction$_k(v_1^{\#}, \dots, v_k^{\#})$ is implied by (respectively equivalent to) (4).
<caption>**Example 2.5** (Result of UseAbsPredicate [4] on Clause 5)</caption>

$$ Increase^{\#}(i, j, a_{size}, a_f) \wedge \left\{ \begin{array}{l} a_{size} \ge 0 \wedge a'_{size} \ge 0 \wedge tmp_2 = tmp_1 + 1 \\ i' = i \wedge j' = j \wedge tmp_1 = select(a_f, i) \\ (a'_{size}, a'_{f}) = (a_{size}, store(a_f, i, tmp_2)) \end{array} \right\} \Rightarrow Check^{\#}(i', j', a'_{size}, a'_{f}) $$

### 4.2.4 Finalize [5] procedure

At this point, there should be no uses of concrete variables or any concrete predicates, but in clauses equivalent to (1). Therefore the Algorithm Finalize [5] simply consists in, for all concrete predicate *P*, *RemoveClause* clauses equivalent to (1) and then *RemoveUnusedPredicates* and *RemoveUnusedVariables* from the quantifier lists, thus removing all concrete predicates and variables.

**Algorithm 5: Finalize [5]:** Wipe concrete variables and predicates out

Input: HornProblem *H*
foreach Predicate *P* ∈ *H* do
  Let *C*<sub>*P*<sub>α</sub></sub> = ∀*arg*, *v*, *v*<sup>#</sup>, *v*<sup>#</sup> ∈ *φ*(*v*) ∧ *P*(*arg*, *v*) ⇒ *P*<sup>#</sup>(*arg*, *v*<sup>#</sup>);
  Let *C*<sub>*P*<sub>γ</sub></sub> = ∀*arg*, *v*, *v*<sup>#</sup>, *v*<sup>#</sup> ∈ *φ*(*v*) ∧ *P*<sup>#</sup>(*arg*, *v*<sup>#</sup>) ⇒ *P*(*arg*, *v*);
  RemoveClause(*H*, *C*<sub>*P*<sub>α</sub></sub>) RemoveClause(*H*, *C*<sub>*P*<sub>γ</sub></sub>); // (1) removed from *H*
end
// No more concrete predicates used
RemoveUnusedPredicates(*H*); // Concrete predicates removed
foreach Clause *C* ∈ *H* do RemoveUnusedVariables(*C*); // Concrete variables removed

Algorithm Finalize [5] is the last step of the Convert [1] and we the final result of Example 2, is given in Example 2.6.

**Soundness and precision analysis** The conversion is sound if *P* is only used in clauses implied by (1): assume the result of the conversion is satisfiable, then the initial problem is satisfiable by taking *P* = *γ*(*P*<sup>#</sup>). The conversion is complete as we do not lose precision by removing clauses.

### 4.2.5 Conclusion

Although there are many steps when using this abstraction technique, the final result is usually close to what one would expect from abstract interpretation techniques. In Example 2.6, we give the result of Algorithm Convert [1] applied on Example 2.

<caption>**Example 2.6** (Result of array abstraction on Example 2 using Algorithm Convert [1])</caption>

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{Types:} & ((i, j, \mathbf{a}_{\text{size}}, \mathbf{a}_f), (i', j', \mathbf{a}'_{\text{size}}, \mathbf{a}'_f)) \in (\text{int} \times \text{int} \times \text{int} \times \text{Function}(\text{Int}, \text{int}))^2 \\
& (\text{tmp}, \text{tmp}_1, \text{tmp}_2) \in \text{int} \times \text{int} \times \text{int} \\
\text{Start}^{\#}(i, j, \mathbf{a}_{\text{size}}, \mathbf{a}_f) & \wedge \mathbf{a}_{\text{size}} \ge 0 \wedge \text{tmp} = \mathbf{a}_{\text{size}} \wedge i \ge \text{tmp} & \Rightarrow \text{false} \\
\text{Start}^{\#}(i, j, \mathbf{a}_{\text{size}}, \mathbf{a}_f) & \wedge \left\{ \begin{array}{l} \mathbf{a}_{\text{size}} \ge 0 \wedge \mathbf{a}'_{\text{size}} \ge 0 \\ \text{tmp} = \mathbf{a}_{\text{size}} \wedge i < \text{tmp} \wedge i' = i \\ j' = \text{select}(\mathbf{a}_f, i) \wedge (\mathbf{a}'_{\text{size}}, \mathbf{a}'_f) = (\mathbf{a}_{\text{size}}, \mathbf{a}_f) \end{array} \right\} & \Rightarrow \text{Increase}^{\#}(i', j', \mathbf{a}'_{\text{size}}, \mathbf{a}'_f) \\
\text{Increase}^{\#}(i, j, \mathbf{a}_{\text{size}}, \mathbf{a}_f) & \wedge \left\{ \begin{array}{l} \mathbf{a}_{\text{size}} \ge 0 \wedge \mathbf{a}'_{\text{size}} \ge 0 \wedge i' = i \wedge j' = j \\ \text{tmp}_1 = \text{select}(\mathbf{a}_f, i) \wedge \text{tmp}_2 = \text{tmp}_1 + 1 \\ (\mathbf{a}'_{\text{size}}, \mathbf{a}'_f) = (\mathbf{a}_{\text{size}}, \text{store}(\mathbf{a}_f, i, \text{tmp}_2)) \end{array} \right\} & \Rightarrow \text{Check}^{\#}(i', j', \mathbf{a}'_{\text{size}}, \mathbf{a}'_f) \\
\text{Check}^{\#}(i, j, \mathbf{a}_{\text{size}}, \mathbf{a}_f) & \wedge \mathbf{a}_{\text{size}} \ge 0 \wedge \text{tmp} = \text{select}(\mathbf{a}_f, i) \wedge j + 1 \ne \text{tmp} & \Rightarrow \text{false}
\end{array}
$$
Although one of the advantages of this abstraction technique is that each conversion is independent, allowing more flexibility when needed, most uses of our framework only require defining three elements to abstract *Source* by *Target* :

1. A function $\phi$ from *Source* to $\mathcal{P}(\mathcal{Target})$.

2. Abstract expressions $abs_{expr}(c_{op}, tmp, args)$ for expressions of the form $tmp = c_{op}(args)$, using $\phi$ such that $tmp = c_{op}(args) \Rightarrow abs_{expr}(c_{op}, tmp, args)$.

3. Expressions $AreAbstractions_k$ such that $(4) \Rightarrow AreAbstraction_k(v_1^#, \dots, v_k^#)$.

The precision analysis our framework entails is divided into three parts:

1. The precision of the Galois connection: how close is $\gamma \circ \alpha$ from $Id$.

2. The precision of abstract expressions: how close is $abs_{expr}(c_{op}, tmp, args)$ from $tmp = c_{op}(args)$.

3. The precision with which we express the image of $\phi$: how close is $AreAbstraction$ from (4).

Inducing one of the main advantage of this framework, a three step reflection:

1. Can I have a more expressive target type ? In the case of infinite data structures to finite
data structure abstractions, we will never have $\gamma \circ \alpha = \mathit{Id}$. However, one can usually improve
precision by making the finite data structure bigger$^{12}$.

2. Can I improve the precision of my abstract expressions ? In most cases we encountered so far, abstract expressions can be complete.

3. Can I improve the precision of *AreAbstractions* ? In all cases we encountered so far, we can define a complete *AreAbstractions*<sub>*k*</sub> for any needed *k*.

In the next Section, we define abstractions to convert problems over unbounded data into problems over bounded data, and we will keep in mind this three step reflection when constructing the conversions.

# 5 To the theory of Horn solvers

Section 3.2 has allowed us to transform a Horn problem over a theory of a programming language into a Horn problem over the *Fundamental* theory that contains the *Basic* theory, functions and possibly many other infinite mathematical structures.

In this section, we focus on abstracting types that belong to the *Fundamental* theory into types of the *Basic* theory. These abstractions are incomplete as we abstract infinite data by finite data and we use the technique in Section 4.2 to give precise abstractions.

## 5.1 Related work: array abstraction

There are several defined abstractions to prove specifications on structured unbounded data and the main focus has been on arrays. In Section 3.2 we transformed arrays to functions with *store* and *select* operations, and in this section, we adapt previous work to our context: we abstract functions and we formalize abstractions within the framework presented in Section 4.2. Doing so increases the generality of previous work as they will work on all Horn problems, and gives us a better precision analysis.

<footnote n="12">¹²This is done repeatedly in Section 5.1, either by using more slices or more distinguished cells</footnote>
### 5.1.1 Cell coalescing

Cell coalescing consists in viewing a function as the set of its values. Intuitively, the store operation just adds the stored value to the set and the select operation just returns the set, giving the Abstraction 2.

<table><caption>**Abstraction 2 (Cell coalescing abstraction of functions)**</caption><thead><tr><th>φ(f ∈ Function&lt;Ind, Val&gt;) = {y ∈ Val | ∃x, y = f(x)}</th></tr></thead><tbody><tr><td><strong>Concrete expression</strong><br>g = store(f, i, v)<br>val = select(f, i)</td><td><strong>Abstract expression</strong><br>∃y<sub>g</sub> ∈ φ(g), (y<sub>g</sub> = v ∨ y<sub>g</sub> ∈ φ(f))<br>val ∈ φ(f)</td></tr><tr><td colspan="2">AreAbstractions<sub>k</sub>(y<sub>1</sub>, ..., y<sub>k</sub>) = true</td></tr></tbody></table>

Cell coalescing is a very imprecise abstraction: the abstract domain does not depend on any indexes whereas the operations do. In practice cell coalescing is very limited as one can not prove cell initialization: $g = store(f, i, v)$; assert(select(g, i) == v); fails.

### 5.1.2 Slices

There are several definitions of slice analysis for functions, but the basic idea is to split the index domain of the function into several segments and apply cell coalescing within each of those sets.

The method to determine the number of sets used and the bounds of each segment vary on the analysis, but the goal on loops is usually to separate indexes that have already gone through the loop and indexes that have not yet. Taking an example where the domain is split into in three segments $] - \infty, j[$, $\{j\}$, $]j, \infty[$, with $j$ a variable, gives Abstraction 3.

<table><caption>**Abstraction 3 (Slice abstraction of functions)**</caption><thead><tr><th>φ(f ∈ Function&lt;Int, Val&gt;) = {(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>) | y<sub>1</sub> ∈ f() &mdash; &mdash; &mdash; j, y<sub>2</sub> = f(j) &mdash; &mdash; &mdash; y<sub>3</sub> ∈ f(j, &infin;[&infin;])</th></tr></thead><tbody><tr><td><strong>Concrete expression</strong><br>g = store(f, i, v)</td><td><strong>Abstract expression</strong><br>∃(y<sub>1</sub><sup>f</sup>, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>) ∈ φ(f), (y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) ∈ φ(g)<br>∧ <span style="font-size: 2em; vertical-align: middle;">{</span> <div style="display: inline-block; vertical-align: middle; text-align: left;"><span style="display: block; border-bottom: 1px solid black; padding: 0 0.2em;">i &lt; j ⇒ ((y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) = (y<sub>1</sub><sup>f</sup>, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>) ∨ (y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) = (v, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>))</span><span style="display: block; padding: 0 0.2em;">i = j ⇒ (y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) = (v, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>)</span><span style="display: block; padding: 0 0.2em;">i &gt; j ⇒ ((y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) = (y<sub>1</sub><sup>f</sup>, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>) ∨ (y<sub>1</sub><sup>g</sup>, y<sub>2</sub><sup>g</sup>, y<sub>3</sub><sup>g</sup>) = (y<sub>1</sub><sup>f</sup>, y<sub>2</sub><sup>f</sup>, v))</span></div></td></tr><tr><td>val = select(f, i)</td><td>∃(y<sub>1</sub><sup>f</sup>, y<sub>2</sub><sup>f</sup>, y<sub>3</sub><sup>f</sup>) ∈ φ(f)<br>∧ <span style="font-size: 2em; vertical-align: middle;">{</span> <div style="display: inline-block; vertical-align: middle; text-align: left;"><span style="display: block; border-bottom: 1px solid black; padding: 0 0.2em;">i &lt; j ⇒ val = y<sub>1</sub><sup>f</sup></span><span style="display: block; padding: 0 0.2em;">i = j ⇒ val = y<sub>2</sub><sup>f</sup></span><span style="display: block; padding: 0 0.2em;">i &gt; j ⇒ val = y<sub>3</sub><sup>f</sup></span></div></td></tr><tr><td colspan="2">AreAbstractions<sub>k</sub>((y<sub>1</sub><sup>1</sup>, y<sub>2</sub><sup>1</sup>, y<sub>3</sub><sup>1</sup>), ..., (y<sub>1</sub><sup>k</sup>, y<sub>2</sub><sup>k</sup>, y<sub>3</sub><sup>k</sup>)) = y<sub>2</sub><sup>1</sup> = ... = y<sub>2</sub><sup>k</sup></td></tr></tbody></table>

Slice abstraction is extremely dependent on how the domain is split into segments: if the current variable read or written to is not a singleton segment, then cell coalescing is applied and we have the same problems. In our framework, we get that the select operation and the store operation are only complete when $i = j$. Therefore, our framework naturally entails that dividing the slices should be done according to the variable being read or written on.
Furthermore, even if some variants of slice abstraction have relations between slices, a sorting invariant would require as many slices as there are cells in the array, which is not a viable option.

### 5.1.3 Cell abstraction

Monniaux and Alberti [2015] made a program to program transformation abstracting a function *f* to its set of cells (*x*, *f*(*x*)). Intuitively, the *store*(*f*, *i*, *v*) operation replaces the couple (*i*, *f*(*i*)) by (*i*, *v*) and *select*(*f*, *i*) returns a value *val* such that the couple (*i*, *val*) is in the cells of *f*, giving Abstraction 4 with abstract *select* Expression 1.

However, the *select* abstract expression is incomplete and the transformation fails to prove simple programs such as array initialization with loop check<fnref n="13" /> does not contain any bugs. In Monniaux and Gonnord [2016], using the added expressiveness of Horn clauses, the *select* abstract expression is replaced by Expression 2, making the *select* expression complete.

<table><caption>**Abstraction 4** (“One distinguished cell abstraction” of functions)</caption><thead><tr><th colspan="2">$\phi(f \in \text{Function}\langle\text{Int}, \text{Val}\rangle) = \{(x, y) | y = f(x)\}$</th></tr></thead><tbody><tr><td>Concrete expression</td><td>Abstract expression</td></tr><tr><td>$g = \text{store}(f, i, v)$</td><td>$\exists(x_g, y_g) \in \phi(g) \wedge \left\{ \begin{array}{l} i = x_g \Rightarrow y_g = v \\ i \neq x_g \Rightarrow (x_g, y_g) \in \phi(f) \end{array} \right.$</td></tr><tr><td>$val = \text{select}(f, i)$</td><td>$\exists(x_f, y_f) \in \phi(f) \wedge \left\{ \begin{array}{l} i = x_f \Rightarrow val = y_f \\ i \neq x_f \Rightarrow y = \top \end{array} \right. \quad (\text{Expression 1})$<br>$\quad (i, val) \in \phi(f) \quad (\text{Expression 2})$</td></tr><tr><td colspan="2">$\text{AreAbstractions}_k((x_1, y_1), \dots, (x_k, y_k)) = \bigwedge_{i,j} x_i = x_j \Rightarrow y_i = y_j$</td></tr></tbody></table>

The abstraction given in Monniaux and Gonnord [2016] has complete abstract expressions and complete *AreAbstractions*. Therefore, precision loss is only due to $\phi$, that is to say that abstract predicates must only depend on one couple (*x*, *f*(*x*)), instead of *f* which represents all couples (*x*, *f*(*x*)). This allows us to express complex states such as $f(0) = 0 \wedge \forall x \neq 0, f(x) = x^2 + 1$ by setting $P: (x, y) \rightarrow (x = 0 \wedge y = 0) \vee (x \neq 0) \wedge y = x^2 + 1$. However, the dependence of predicates on only one couple (*x*, *f*(*x*)) does not allow the expressiveness of states such as *f* is increasing (sortedness of arrays).

Monniaux and Gonnord [2016] use the principle of many distinguished cells to solve the problem. The idea is fairly simple: enlarge the abstract domain to several couples (*x*, *f*(*x*)) so that predicates can depend on relations between cells. For example, two distinguished cells can express that *f* is increasing: $P: ((x^1, y^1), (x^2, y^2)) \rightarrow x^1 < x^2 \Rightarrow y^1 \leq y^2$. A small optimization that Monniaux and Gonnord [2016] suggest is to order the cells to avoid repetition. Abstraction 5 describes the technique for two distinguished cells.

The main expressiveness limit of distinguished cell abstraction is program states that depend on an unbounded number of cells. For example, the program state “The sum of all the cells of the function is equal to 42” depends on all the cells of the function and the abstract predicate will always be false. This seems to be a general limit of Horn clauses on bounded data and we believe there is no abstraction with better expressiveness.

<footnote n="13">¹³This is Example 1 with a loop within the user specifications instead of a rand().</footnote>
<table><caption>**Abstraction 6** (insert and erase expressions for one distinguished cell abstraction)</caption><thead><tr><th colspan="2">$\phi(f \in \text{Function}\langle\text{Int}, \text{Val}\rangle) = \{(x, y) | y = f(x)\}$</th></tr><tr><th>Concrete expression</th><th>Abstract expression</th></tr></thead><tbody><tr><td>$g = \text{insert}(f, i, v)$</td><td>$\exists(x_g, y_g) \in \phi(g) \land \left\{ \begin{array}{l} x_g < i \Rightarrow (x_g, y_g) \in \phi(f) \\ x_g = i \Rightarrow y_g = v \\ x_g > i \Rightarrow (x_g - 1, y_g) \in \phi(f) \end{array} \right.$</td></tr><tr><td>$g = \text{erase}(f, i)$</td><td>$\exists(x_g, y_g) \in \phi(g) \land \left\{ \begin{array}{l} x_g < i \Rightarrow (x_g, y_g) \in \phi(f) \\ x_g \ge i \Rightarrow (x_g + 1, y_g) \in \phi(f) \end{array} \right.$</td></tr><tr><td colspan="2">$\text{AreAbstractions}_k((x_1, y_1), \dots, (x_k, y_k)) = \bigwedge_{i,j} x_i = x_j \Rightarrow y_i = y_j$</td></tr></tbody></table>

This is a major contribution as *Function<Ind, Val>* with the *store*, *select*, *insert* and *erase* operations, enables us to abstract C++ containers: vectors, lists, deque, maps, multimaps, sets, multisets... We can even abstract compound structures such as *list<array<\*int\>*>* by applying this abstraction recursively.

Furthermore, the precision limit of the abstraction is not a big problem on such structures as most algorithms on such structures do not require an unbounded number of distinguished cells: most invariants only depend on the relation index to value and not so much on relations between many cells. As with arrays, we have enough precision to prove many sorting algorithms, searching algorithms, ... The sortedness of *insertion sort* can be proved through Example 3, which represents a simplified output of Algorithm 1 with two distinguished cell abstraction.

We have given a general technique to abstract linear data structures. In the next section, we give research directions to abstract non linear data structures.

### 5.2.2 Research directions: trees, graphs, ...

Our whole technique relies on Abstraction 4. Intuitively, the *select* and *store* operations allow us to abstract arbitrary containers that do not change structure. In Abstraction 6, we extended that scheme to linear containers by masking the change of structure through an index shift.

We generalize this scheme and define abstractions on containers of type *Val* as *Function<\*L, Val>* where \*L is a labeling of the structure we abstract. In the case of arrays and lists, \*L is *Int*.

We must then abstract operations that modify the structure of \*L by operations on \*L. For example, in lists we abstracted the *erase* operation by a shift in the indexes, that is to say as a shift in the labeling. For example, binary trees have several classical labelings Rastello [2012]:

* The labeling for which we already have abstractions is *list<\*Bool>*: each node position is described by a list of left/right indications from the top node. Insertions and deletions within the tree are mapped to operations on labels: insertions and deletions on *list<\*Bool>* correspond to insertions and deletions of a tree using *list<\*Bool>* as label type. However, this abstraction fails: The domain is *Function<\*Function<\*Int, \*Bool>, \*Val>* and after abstraction, the abstract value of a tree becomes several triples (*depth*, *right/left*, *val*) depending on the number of distinguished cells used. We can not express the parent/child relationships between two such triples, which is necessary for many algorithm on trees.

* Labelings from depth or breadth first search algorithms seem adequate: insertion and deletion correspond to index shifts and the precision loss is small: we can express parent/child relations with two distinguished cells and thus prove many algorithms. The main issue with this abstraction is that a given labeling corresponds to many trees, creating a loss of precision.
Example 3 (Insertion sort)

(a) C++ code with Section 3.2 conversion in comments

```cpp
std::list<int> insertion_sort(const std::list<int>& l) {
    // lsize ≥ 0
    std::list<int> res;
    // ressize ≥ 0
    std::list<int>::const_iterator lit = l.end();
    // lit' = 0
    while(lit != l.end()) {
        // lit ≠ lsize
        int val = *lit;
        // val' = select(resf, lit)
        std::list<int>::iterator resit = res.end();
        // resit' = 0
        while(resit != res.end()) {
            // resit ≠ ressize
            int read = *resit;
            // read' = select(resf, resit)
            if (read > val) break;
            // read > val ⇒ resInsert
            resit++;
            // resit' = resit + 1
        }
        // resit = ressize
        res.insert(resit, val);
        // res' size = res size + 1 ∧ res' f = insert(resf, resit, val)
        lit++;
        // lit' = lit + 1
    }
    // lit = lsize
    return res;
}
// x < y ∧ resf(x) > resf(y) ⇒ false
```

(b) Final result of function abstraction with two distinguished cells

<table><tr><td>lsize ≥ 0 ∧ l<sup>1</sup><sub>x</sub> &lt; l<sup>2</sup><sub>x</sub></td><td>⇒ Start(lsize, l<sup>1</sup><sub>x</sub>, l<sup>1</sup><sub>y</sub>, l<sup>2</sup><sub>x</sub>, l<sup>2</sup><sub>y</sub>)</td></tr><tr><td>Start(lsize, l<sup>1</sup><sub>x</sub>, l<sup>1</sup><sub>y</sub>, l<sup>2</sup><sub>x</sub>, l<sup>2</sup><sub>y</sub>) ∧ ressize ≥ 0 ∧ res<sup>1</sup><sub>x</sub> &lt; res<sup>2</sup><sub>x</sub> ∧ ...</td><td>⇒ lit_init(..., ressize, res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>)</td></tr><tr><td>lit_init(...) ∧ lit' = 0 ∧ ...</td><td>⇒ l_While(...)</td></tr><tr><td>l_While(...) ∧ lit ≠ lsize ∧ ...</td><td>⇒ val_init(...)</td></tr><tr><td>val_init(..., l<sup>1</sup><sub>x</sub>, l<sup>1</sup><sub>y</sub>, l<sup>2</sup><sub>x</sub>, l<sup>2</sup><sub>y</sub>,...) ∧ lit ≠ l<sup>1</sup><sub>x</sub> ∧ val_init(..., lit, val', l<sup>2</sup><sub>x</sub>, l<sup>2</sup><sub>y</sub>,...) ∧ ...</td><td>⇒ resit_init(...)</td></tr><tr><td>val_init(..., l<sup>1</sup><sub>x</sub>, l<sup>1</sup><sub>y</sub>, l<sup>2</sup><sub>x</sub>, l<sup>2</sup><sub>y</sub>,...) ∧ lit = l<sup>1</sup><sub>x</sub> ∧ val' = l<sup>1</sup><sub>y</sub> ∧ ...</td><td>⇒ resit_init(...)</td></tr><tr><td>resit_init(...) ∧ resit' = 0 ∧ ...</td><td>⇒ res_While(...)</td></tr><tr><td>res_While(...) ∧ resit ≠ ressize ∧ ...</td><td>⇒ read_init(...)</td></tr><tr><td>read_init(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit ≠ res<sup>1</sup><sub>x</sub> ∧ read_init(..., resit, read', res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ ...</td><td>⇒ If(...)</td></tr><tr><td>read_init(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit = res<sup>1</sup><sub>x</sub> ∧ read' = res<sup>1</sup><sub>y</sub> ∧ ...</td><td>⇒ If(...)</td></tr><tr><td>If(...) ∧ read > val ∧ ...</td><td>⇒ res_insert(...)</td></tr><tr><td>If(...) ∧ read ≤ val ∧ ...</td><td>⇒ res_incr(...)</td></tr><tr><td>res_incr(...) ∧ resit' = resit + 1 ∧ ...</td><td>⇒ res_While(...)</td></tr><tr><td>res_While(...) ∧ resit = ressize ∧ ...</td><td>⇒ res_insert(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit > res<sup>2</sup><sub>x</sub> ∧ res'<sub>size</sub> = ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit = res<sup>2</sup><sub>x</sub> ∧ res'<sub>y</sub> = val ∧ ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit = res<sup>2</sup><sub>x</sub> ∧ res'<sub>x</sub> = res<sup>2</sup><sub>x</sub> ∧ res'<sub>y</sub> = val ∧ res'<sub>x</sub> = res<sup>2</sup><sub>x</sub> + 1 ∧ ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit < res<sup>2</sup><sub>x</sub> ∧ res'<sub>x</sub> = res<sup>2</sup><sub>x</sub> + 1 ∧ ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit = res<sup>2</sup><sub>x</sub> ∧ res'<sub>x</sub> = res<sup>2</sup><sub>x</sub> + 1 ∧ res'<sub>y</sub> = val ∧ ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>res_insert(..., res<sup>1</sup><sub>x</sub>, res<sup>1</sup><sub>y</sub>, res<sup>2</sup><sub>x</sub>, res<sup>2</sup><sub>y</sub>,...) ∧ resit < res<sup>2</sup><sub>x</sub> ∧ res'<sub>x</sub> = res<sup>2</sup><sub>x</sub> + 1 ∧ res'<sub>x</sub> = res<sup>1</sup><sub>x</sub> + 1 ∧ ...</td><td>⇒ lit_incr(...)</td></tr><tr><td>lit_incr(...) ∧ lit' = lit + 1 ∧ ...</td><td>⇒ l_While(...)</td></tr><tr><td>l_While(...) ∧ lit = lsize ∧ ...</td><td>⇒ Return(...)</td></tr><tr><td>Return(...) ∧ 0 ≤ res<sup>1</sup><sub>x</sub> &lt; res<sup>2</sup><sub>x</sub> &lt; res<sub>size</sub> ∧ res<sup>1</sup><sub>y</sub> &gt; res<sup>2</sup><sub>y</sub> ⇒ false</td><td>/* Sortedness */</td></tr></table>

We use $l_x^1, l_y^1, l_x^2, l_y^2$ as an abstraction of $l_f$ and $res_x^1, res_y^1, res_x^2, res_y^2$ for $res_f$. To increase readability, disjunctions within expressions are separated into several clauses, equalities have been propagated, and the final condition has been simplified.
We have not yet implemented any of these abstractions and we leave the proper analysis, imple-
mentation and tests of these abstractions for future work.

# 6 Implementation and experiments

**Implementation** We separated the implementation in two parts:

* The front end that takes as input a mini-Java program (a variation of WHILE with array, lists, and assertions), and outputs a SMTLIB2 file<sup>14</sup> describing a Horn problem in a theory close to *Fundamental*.

* The back-end that takes as input a SMTLIB2 file describing a Horn problem in a theory close to *Fundamental* and outputs a SMTLIB2 file describing a Horn problem in the *Basic* theory.

The front end is an adaptation of the Vaphor tool (Monniaux and Gonnord [2016]) to which we added lists, multidimensional arrays and composed operations<fnref n="15" />. We entirely developed the back-end from scratch following the technique described in Section 4.2 in 1.5k lines of Ocaml. There are slight differences as the theory around *AreAbstractions* had not been developed yet, but the overall result for function abstraction is equivalent.

Furthermore, the back-end is modular and independent of the front end, and can be used to test
many other abstractions. The main purpose of the implementation is to serve as proof of concept
for abstractions to come so that abstractions can then be implemented within Horn solvers or code
analysis tools such as SeaHorn.

Various tools can solve systems of Horn clauses in the *Basic* theory. In this work, we tried Z3<sup>16</sup> with the PDR fixed point solver [Hoder and Bjørner, 2012], Z3 with the SPACER solver [Komu-ravelli et al., 2013, 2014],<sup>17</sup> and ELDARICA[Rümmer et al., 2013].<sup>18</sup> Since program verification is undecidable, such tools, in general, may fail to terminate, or may return “unknown”.

**Experiments** We tested our analyzer on several examples from the literature:

* array benchmarks from the literature, [Dillig et al., 2010], [Bjørner et al., 2013], are in Table 1.

* classical algorithms on arrays and lists, including *bubble sort* and *insertion sort* in Table 2.

There has been no real tests on Horn problems that were not induced by programs as we have not been able to find examples of such Horn problems. The output is equivalent to the experiments of Monniaux and Gonnord [2016], the abstraction being the same.

**Conversion tool limitations** The front end suffers from limitations due to the Vaphor tool as the code was not completely rewritten:

* It does not deal with types other than integers, booleans, arrays and lists.

* Although it deals with multidimensional arrays, it does not deal with compound structures such as lists of arrays.

**Horn solver limitations** The Horn problems we retrieve from our technique are very close to those of Monniaux and Gonnord [2016] and suffer from the same Horn solver limitation: unreliable solving times as Horn solvers rely on backtracking and a simple change in the variable declaration

<footnote n="14"><sup>14</sup>http://smtlib.cs.uiowa.edu/</footnote>

<footnote n="15"><sup>15</sup>The VapHor tool used edge abstraction and could not deal with composed operations.</footnote>

<footnote n="16"><sup>16</sup>https://github.com/Z3Prover hash 7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152; due to various problems we pre-ferred not to use results from later versions.</footnote>

<footnote n="17"><sup>17</sup>https://bitbucket.org/spacer/code hash 7e1f9af01b796750d9097b331bb66b752ea0ee3c</footnote>

<footnote n="18"><sup>18</sup>https://github.com/uuverifiers/eldarica/releases/tag/v1.1-rc</footnote>
<caption>Table 1: Comparison on the array benchmarks of [Dillig et al., 2010].</caption>

(Average) timing are in seconds, CPU time. Abstraction with $N = 1$. “sat” means the property was proved, “unsat” that it could not be proved. “hints” means that some invariants had to be manually supplied to the solver (e.g. even/odd conditions). A star means that we used another version of the solver. Timeout was 5 mn unless otherwise noted. The machine has 32 i3-3110M cores, 64 GiB RAM, C/C++ solvers were compiled with gcc 4.8.4, the JVM is OpenJDK 1.7.0-85.

<table><caption>Table 2: Other array-manipulating programs, including various sorting algorithms.</caption><thead><tr><th rowspan="2">Benchmark</th><th colspan="2">Z3/PDR</th><th colspan="2">Z3/Spacer</th><th colspan="2">Eldarica</th><th rowspan="2">Comment</th></tr><tr><th>Res</th><th>Time</th><th>Res</th><th>Time</th><th>Res</th><th>Time</th></tr></thead><tbody><tr><td colspan="8" style="text-align: left;">Correct problems, “sat” expected</td></tr><tr><td>array copy</td><td>sat</td><td>0.42</td><td>sat</td><td>0.23</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array init2d</td><td>sat</td><td>1.12</td><td>sat</td><td>0.44</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array init2i</td><td>sat</td><td>0.56</td><td>sat</td><td>0.22</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array initcte</td><td>sat</td><td>0.15</td><td>sat</td><td>0.08</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array partialcopy</td><td>sat</td><td>0.46</td><td>sat</td><td>0.60</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array reverse</td><td>sat</td><td>82.32</td><td>sat</td><td>0.26</td><td>sat</td><td>36.61</td><td></td></tr><tr><td>array strcpy</td><td>sat*</td><td>4.31</td><td>sat</td><td>0.30</td><td>sat</td><td>18.21</td><td></td></tr><tr><td>array strlen</td><td>sat</td><td>0.20</td><td>sat</td><td>0.11</td><td>sat</td><td>27.39</td><td></td></tr><tr><td>array swapncopy</td><td>sat</td><td>1.73</td><td>sat</td><td>0.86</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>arrayappend</td><td>sat</td><td>61.40</td><td>sat</td><td>0.78</td><td>sat</td><td>17.17</td><td></td></tr><tr><td>arrayfind</td><td>sat</td><td>0.20</td><td>sat</td><td>0.11</td><td>sat</td><td>10.76</td><td></td></tr><tr><td>arrayfindnonnull</td><td>sat</td><td>0.28</td><td>sat</td><td>0.25</td><td>sat</td><td>14.10</td><td></td></tr><tr><td>memcpy</td><td>sat</td><td>0.44</td><td>sat</td><td>0.23</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array initeven</td><td>timeout(300s)</td><td></td><td>timeout(300s)</td><td></td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array initeven hinted</td><td>sat</td><td>0.03</td><td>sat</td><td>0.02</td><td>sat</td><td>4.74</td><td>Hinted</td></tr><tr><td>array swapncopy twice</td><td>timeout(300s)</td><td></td><td>sat</td><td>15.46</td><td>timeout(300s)</td><td></td><td></td></tr><tr><td>array swapncopy twice hinted</td><td>sat</td><td>0.13</td><td>sat</td><td>0.08</td><td>sat</td><td>12.64</td><td>Hinted</td></tr><tr><td>mergeinterleave</td><td>sat</td><td>8.49</td><td>sat</td><td>207.02</td><td>sat</td><td>77.95</td><td></td></tr><tr><td>mergeinterleave hinted</td><td>sat</td><td>0.19</td><td>sat</td><td>0.05</td><td>sat</td><td>10.54</td><td>Hinted</td></tr><tr><td colspan="8" style="text-align: left;">Incorrect problems, “unsat” expected</td></tr><tr><td>array copyodd buggy</td><td>unsat</td><td>0.05</td><td>unsat</td><td>0.02</td><td>unsat</td><td>7.29</td><td></td></tr><tr><td>array initeven buggy</td><td>unsat</td><td>0.05</td><td>unsat</td><td>0.03</td><td>unsat</td><td>5.50</td><td></td></tr><tr><td>array reverse buggy</td><td>unsat</td><td>0.52</td><td>unsat</td><td>0.71</td><td>unsat</td><td>57.69</td><td></td></tr><tr><td>array swapncopy buggy</td><td>unsat</td><td>0.93</td><td>unsat</td><td>0.19</td><td>unsat</td><td>32.08</td><td></td></tr><tr><td>mergeinterleave buggy</td><td>unsat</td><td>0.54</td><td>unsat</td><td>0.22</td><td>unsat</td><td>26.77</td><td></td></tr></tbody></table>

A star means that we used a previous version of the solver.

<table><thead><tr><th rowspan="2">Benchmark</th><th colspan="2">Z3/PDR</th><th colspan="2">Z3/Spacer</th><th colspan="2">Eldarica</th><th rowspan="2">Distinct number</th></tr><tr><th>Res</th><th>Time</th><th>Res</th><th>Time</th><th>Res</th><th>Time</th></tr></thead><tbody><tr><td>bin search</td><td>sat</td><td>0.38</td><td>timeout(300s)</td><td></td><td>Exception</td><td>N=1</td><td></td></tr><tr><td>find mini</td><td>sat</td><td>2.99</td><td>sat</td><td>1.16</td><td>sat</td><td>58.97</td><td>N=1</td></tr><tr><td>bubble sort</td><td>sat</td><td>4.42</td><td>sat</td><td>3.17</td><td>sat</td><td>68.86</td><td>N=2</td></tr><tr><td>insert sort</td><td>sat*</td><td>146.42</td><td>timeout(300s)</td><td></td><td>timeout(300s)</td><td>N=2</td><td></td></tr></tbody></table>

order, or in the pseudo-random number generator can change execution time by over a factor 100. Guiding the solver by asserting simple invariants (e.g. $0 \le k < i$ for a loop from $k$ to $i-1$) greatly improves the reliability of the solvers.

Like Monniaux and Gonnord [2016], we believe that solving times should not be regarded too closely: research on Horn solvers is recent and the solving times might change drastically in the years to come through the combination of abstract interpretation and SMT solving. The purpose of our experimental evaluation is not to benchmark solvers relative to each other, but to show that our abstraction, even though it is incomplete, is powerful enough to lead to fully automated proofs of correctness of nontrivial manipulations of linear data structures, including sorting algorithms.

# 7 Conclusion and perspectives

We proposed a generic approach to verify specifications on programs containing unbounded data structures. This approach has been applied to arrays and lists: arrays have been fully tested
on algorithms requiring non trivial invariants, such as sorting algorithms, and lists have been
implemented but not thoroughly tested. We expect to have solid test results on lists in the very
near future.

The limitations of the approach can be divided into three categories: limitations due to program conversions and mainly pointers as described in Section 3.2, limitations due to unbounded data abstraction as explained in Section 5 and limitations due to Horn solvers.

Converting programs in real world programming languages to Horn clauses over a theory that does not involve memory is a tough task and the work in Section 3.2 does not cover it. In fact, we expect this step to be at least as hard as converting a program into a functional language as it requires the static analyzer to abstract pointers. There is active research on the topic: alias analyses, shape analyses, separation logic, ... and tools such as SeaHorn and FramaC, and we do not expect this limitation to be the main issue.

The second limitation has been the main focus of our work. We have succeeded in defining what are
probably the best possible abstractions on Horn clauses for lists and arrays and gave a framework
as well as research directions to abstract general unbounded data structures. Furthermore, we gave
an implementation and experiments that show that our abstractions succeed in proving non trivial
algorithms.

However, our technique can not prove specifications such as "the sum of the array is equal to 42" as this requires a number of distinguished cells equal to the size of the array. We believe this is a limit of abstract interpretation and that such specifications can not be proven through the use of abstract interpretation only, or at least without major drawbacks. We intend to investigate another technique which consists in expressing local changes instead of global changes: we may not be able to express that the sum of an array is equal to 42, but we can express that the store operation adds *stored_val* − *old_val* to the sum of the array. By introducing a variable representing the sum of the array and modifying it at each *store* operation, we can prove that the sum of the array is equal to 42. A similar technique has been applied in Monniaux and Gonnord [2016] to prove that the multiset of values is unchanged by a sorting algorithm.

Another issue is extending the abstract interpretation of unbounded data structures into bounded
data structure. We succeeded for lists and arrays and we seem close to succeeding for trees. How-
ever, finding abstract interpretation on graphs that could prove shortest path algorithms remains
an untouched research topic. In the near future, we intend to analyze, implement and test the tree
abstraction using depth/breadth first search labeling described in Section 5.2.2.

Finally, a major issue of our approach is that Horn solvers still have unreliable solving times. The main reason for this issue is that Horn solvers calculate predicates by backtracking and refining predicates when the current solution is unsatisfiable. This technique is subject to huge variance as choosing the value of predicates when backtracking occurs is done through heuristics.

There has been major improvement on Horn solvers in the past years and we expect improvements
in the years to come. Mainly, we expect that invariants that can be calculated through abstract
interpretation, for example in the polyhedron model, will not require backtracking and predicate
refinement.
References

N. Bjørner, K. McMillan, and A. Rybalchenko. On solving universally quantified Horn clauses. In *Static Analysis Symposium (SAS)*, pages 105–125, 2013. doi: 10.1145/2695664.2695784.

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Principles of Programming Languages (POPL)*, pages 238–252, 1977. doi: 10.1145/512950.512973.

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In *Principles of Programming Languages (POPL)*, pages 84–96, 1978. doi: 10.1145/512760.512770.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTRÉE analyzer. In *European symposium on programming (ESOP)*, number 3444 in Lecture Notes in Computer Science, pages 21–30, 2005. ISBN 978-3-540-25435-5. doi: 10.1007/978-3-540-31987-0_3.

I. Dillig, T. Dillig, and A. Aiken. Fluid updates: Beyond strong vs. weak updates. In *European Conference on Programming Languages and Systems (ESOP)*, pages 246–266, 2010. doi: 10.1007/978-3-642-11957-6_14.

K. Hoder and N. Bjørner. Generalized property directed reachability. In *Theory and Applications of Satisfiability Testing (SAT)*, volume 7317 of LNCS, pages 157–171. Springer, 2012. ISBN 978-3-642-31611-1. doi: 10.1007/978-3-642-31612-8_13.

N. D. Jones and S. S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In *Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '82, pages 66–74, New York, NY, USA, 1982. ACM. ISBN 0-89791-065-6. doi: 10.1145/582153.582161. URL http://doi.acm.org/10.1145/582153.582161.

A. Komuravelli, A. Gurfinkel, S. Chaki, and E. M. Clarke. Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In *Computer-aided verification (SAS)*, volume 8044, pages 846–862. Springer, 2013. ISBN 978-3-642-39798-1. doi: 10.1007/978-3-642-39799-8_59.

A. Komuravelli, A. Gurfinkel, and S. Chaki. Smt-based model checking for recursive programs. In A. Biere and R. Bloem, editors, *Computer-aided verification (SAS)*, volume 8559 of LNCS, pages 17–34. Springer, 2014. ISBN 978-3-319-08866-2. doi: 10.1007/978-3-319-08867-9_2.

D. Monniaux and F. Alberti. A simple abstraction of arrays and maps by program translation. In *Static analysis (SAS)*, volume 9291 of Lecture Notes in Computer Science, pages 217–234. Springer Verlag, 2015. ISBN 978-3-662-48287-2. doi: 10.1007/978-3-662-48288-9. URL https://hal.archives-ouvertes.fr/hal-01162795.

D. Monniaux and L. Gonnord. Cell morphing: from array programs to array-free Horn clauses. Working paper, Apr. 2016. URL https://hal.archives-ouvertes.fr/hal-01206882.

F. Rastello. On Sparse Intermediate Representations: Some Structural Properties and Applications to Just-In-Time Compilation. University works, Dec. 2012. URL https://hal.inria.fr/hal-00761555. Habilitation à diriger des recherches, École normale supérieure de Lyon.
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In *Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science*, LICS '02, pages 55-74, Washington, DC, USA, 2002. IEEE Computer Society. ISBN 0-7695-1483-9. URL http://dl.acm.org/citation.cfm?id=645683.664578.

P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for Horn-clause verification. In N. Sharygina and H. Veith, editors, *Computer-aided verification (CAV)*, volume 8044 of *LNCS*, pages 347-363. Springer, 2013. ISBN 978-3-642-39798-1. doi: 10.1007/978-3-642-39799-8_24.