# A Verification Toolkit for Numerical Transition Systems Tool Paper ⋆

Hossein Hojjat, Florent Garnier, Radu Iosif, Filip Konečny, Viktor Kuncak, Philipp Rümmer

► To cite this version:

Hossein Hojjat, Florent Garnier, Radu Iosif, Filip Konečny, Viktor Kuncak, et al. A Verification Toolkit for Numerical Transition Systems Tool Paper ⋆. 18th International Symposium on Formal Methods, Aug 2012, Paris, France. hal-01418901

HAL Id: hal-01418901

https://hal.science/hal-01418901

Submitted on 17 Dec 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.

Public Domain
# A Verification Toolkit for Numerical Transition Systems

## Tool Paper*

Hossein Hojjat¹, Florent Garnier², Radu Iosif²,
Filip Konečný², Viktor Kuncak¹, and Philipp Rümmer³

¹ Swiss Federal Institute of Technology Lausanne (EPFL)

² Verimag, Grenoble, France

³ Uppsala University, Sweden

**Abstract.** This paper reports on an effort to create benchmarks and a toolkit for rigorous verification problems, simplifying tool integration and eliminating ambiguities of complex programming language constructs. We focus on *Integer Numerical Transition Systems* (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We describe the syntax, semantics, a front-end, and a first release of benchmarks for such transition systems. Furthermore, we present FLATA and ELDARICA, two new verification tools for INTS. The FLATA system is based on precise acceleration of the transition relation, while the ELDARICA system is based on predicate abstraction with interpolation-based counterexample-driven refinement. The ELDARICA verifier uses the PRINCESS theorem prover as a sound and complete interpolating prover for Presburger arithmetic. Both systems can solve several examples for which previous approaches failed and present a useful baseline for verifying integer programs. Our infrastructure is publicly available; we hope that it will spur further research, benchmarking, competitions, and synergistic communication between verification tools.

## 1 Introduction

Common representation formats, benchmarks, and tool competitions have helped research in a number of areas, including constraint solving, theorem proving, and compilers. To bring such benefits to the area of software verification, we are proposing a standardized logical format for programs, in terms of hierarchical infinite-state transition systems. The advantage of using a formally defined common format is avoiding ambiguities of programming language semantics and helping to separate semantic modeling from designing verification algorithms.

This paper focuses on systems whose transition relation is expressed in Presburger arithmetic. Integer Numerical Transition Systems, (denoted INTS throughout this paper), also known as counter automata, counter systems, or counter machines, are an infinite-state extension of the model of finite-state *boolean transition systems*, a model extensively used in the area of software verification [10]. The interest for INTS comes from the fact that they can encode various classes of systems with unbounded (or very large) data domains, such as hardware circuits, cache memories, or software systems with variables of non-primitive types, such as integer arrays, pointers and/or recursive data structures.

Any Turing-complete class of systems can, in principle be simulated by an INTS [12]. Despite this expressiveness, a number of recent works have revealed cost-effective approximate reductions of verification problems for several classes of complex systems to decision problems, phrased in terms on INTS. Examples of systems that can be effectively verified by means of integer programs include: specifications of hardware components [14], programs with singly-linked lists [2], trees [8], and integer arrays [3]. Hence the growing interest for analysis tools working on INTS.

<footnote>* Supported in part by the Rich Model Toolkit initiative, http://richmodels.org</footnote>
<figure><img src="image_1.png" /><figcaption>**Fig. 1.** Example Program and its Numerical Transition System (NTS) Representation. By convention, if a variable *v* does not appear in the transition relation formula, we implicitly assume the frame condition *v* = *v'* is conjoined with the formula.</figcaption></figure>

We believe that robustly handling a wide variety of patterns of programming with integers is essential for building robust verification tools. As an example, consider the program in Figure 1(a). Most programmers would have little difficulty observing that the assertion will always succeed, but many tools, including non-relational abstract interpretation, as well as predicate abstraction with arbitrary interpolation can fail to prove the assertion to hold [11]. The integer numerical transition system for this program is in Figure 1(b). We have developed a toolkit for producing and manipulating such representations, as well as two very different analyzers that can analyze such transition systems. Both analyzers, ELDARICA and FLATA, in fact succeed for this, as well as for several other interesting examples. In other cases, however, our experiments show that these two techniques are complementary, so a user benefits from two different technologies that use the same input format.

## 2 The INTS Infrastructure

We have developed a toolkit for rigorous automated verification of programs in INTS format. The unifying component is the INTS library^4, which defines the syntax of the INTS representation by providing a parser and a library of abstract syntax tree classes. For the purposes of this paper, the INTS syntax can be considered to be just a textual description of a control flow graph labeled by Presburger arithmetic formulae, as e.g., the one in Figure 1 (b).

There are several components built using the INTS format, either as input, output or both. The INTS library is designed in order to support relatively easy bridging with new tools, which can be either front-ends (translators from mainstream programming languages into INTS), back-ends (verifier tools), or both. Currently, there exists tools to

<footnote>^4 http://richmodels.epfl.ch/ntscomp/ntslib</footnote>
generate INTS from sequential and concurrent C, Scala, and Verilog. We present two tools that can verify INTS programs: FLATA and Eldarica.

**Flata verifier.** FLATA<fnref n="5" /> is a verification tool for hierarchical non-recursive INTS models. The verification technique used in FLATA is based on computing transitive closures of loops labeled by conjunctive transition relations. The three main classes of integer relations for which transitive closures can be computed precisely in finite time are: (1) *difference bounds constraints*, (2) *octagons*, and (3) *finite monoid affine transformations*. For these three classes, the transitive closures can be effectively defined in Presburger arithmetic.

The transitive closure computation is integrated in a semi-algorithmic method for computing the summary relation of an individual INTS. This algorithm builds the relation incrementally, by eliminating control states and composing incoming with outgoing relations. The verification method is *modular*: the tool computes the summary relation for each INTS independently of its calling context, thus avoiding the overhead of procedure inlining.

**Eldarica verifier.** ELDARICA implements predicate abstraction with Counter-Example Guided Abstraction Refinement (CEGAR). It generates an abstract reachability tree (ART) of the system on demand, using lazy abstraction [10] with Cartesian abstraction, and uses interpolation to refine the set of predicates [9]. ELDARICA uses caching of the previously explored states and formulae to prevent unnecessary reconstruction of tree. On demand, large block encoding [1] can be performed to reduce the number of calls to the interpolating theorem prover.

Eldarica refines abstractions with the help of *Craig Interpolants*, extracted from infeasibility proofs for spurious counterexamples. A complete interpolation procedure for (quantifier-free) Presburger arithmetic was proposed in [5], and has been implemented in the Princess prover [13] that we use in Eldarica. In this approach, interpolants are extracted from unsatisfiability proofs of conjunctive formulae, by recursively annotating the proof with partial and intermediate interpolants.

## 3 Experimental Comparison of the FLATA and ELDARICA Tools

We next show the benefits of INTS on comparing the performance of the FLATA and ELDARICA tools. This experimental analysis also points to the current strengths and weaknesses of the two tools we are developing. We have considered six sets of examples, extracted automatically from different sources: (a) C programs with arrays provided as examples of divergence in predicate abstraction [11], (b) INTS extracted from programs with singly-linked lists by the L2CA tool [2], (c) INTS extracted from VHDL models of circuits following the method of [14], (d) verification conditions for programs with arrays, expressed in the SIL logic of [3] and translated to INTS, (e) C programs provided as benchmarks in the NECLA static analysis suite, and (f) C programs with asynchronous procedure calls translated into INTS using the approach of [7] (the examples with extension `.optim` are obtained via an optimized translation method [6]).

The execution times are relative to an XXXX architecture. We noticed that the two tools behaved in a complementary way. In some cases (in particular on the (a) examples) the predicate abstraction method fails due to an unbounded number of loop unrollings required by refinement. In these cases, acceleration was capable to find the needed invariant rather quickly. On the other hand, in particular on the (f) examples, the acceleration

<footnote n="5">⁵ http://www-verimag.imag.fr/FLATA.html</footnote>
approach was unsuccessful in reducing loops with linear but non-octagonal relations. In these cases, the predicate abstraction found the needed Presburger invariants for proving correctness, and error traces, for the erroneous examples.

<table><caption>**Fig. 2.** Benchmarks for Flata and Eldarica. The letter after the model name distinguishes Correct from Erratic models. Items with “-” led to a timeout for the respective tool.</caption><thead><tr><th>Model</th><th colspan="2">Time [s]</th><th>Model</th><th colspan="2">Time [s]</th><th>Model</th><th colspan="2">Time [s]</th></tr><tr><th>(a) Examples from [11]</th><th>Flata</th><th>Eld.</th><th>(c) VHDL models from [14]</th><th>Flata</th><th>Eld.</th><th>(f) Examples from [7]</th><th>Flata</th><th>Eld.</th></tr></thead><tbody><tr><td>anubhav (C)</td><td>0.4</td><td>2.5</td><td>counter (C)</td><td>0.1</td><td>2.2</td><td>h1 (E)</td><td>-</td><td>13.8</td></tr><tr><td>copy1 (E)</td><td>1.0</td><td>9.0</td><td>register (C)</td><td>0.1</td><td>1.3</td><td>h1.optim (E)</td><td>0.5</td><td>2.7</td></tr><tr><td>couso (C)</td><td>0.3</td><td>-</td><td>synlifo (C)</td><td>14.7</td><td>57.3</td><td>h1h2 (E)</td><td>-</td><td>35.3</td></tr><tr><td>loop1 (C)</td><td>0.3</td><td>2.4</td><td colspan="3"><b>(d) Verification conditions for array programs [3]</b></td><td>h1h2.optim (E)</td><td>0.7</td><td>5.2</td></tr><tr><td>loop (C)</td><td>0.3</td><td>1.3</td><td>rotation_vc.1 (C)</td><td>0.5</td><td>2.3</td><td>simple (E)</td><td>-</td><td>11.9</td></tr><tr><td>scan (E)</td><td>1.5</td><td>-</td><td>rotation_vc.2 (C)</td><td>0.8</td><td>2.4</td><td>x simple.optim (E)</td><td>0.5</td><td>2.7</td></tr><tr><td>string_concat1 (E)</td><td>3.1</td><td>-</td><td>rotation_vc.3 (C)</td><td>0.7</td><td>0.4</td><td>test0 (C)</td><td>-</td><td>36.2</td></tr><tr><td>string_concat (E)</td><td>3.0</td><td>-</td><td>rotation_vc.1 (E)</td><td>0.6</td><td>1.5</td><td>test0.optim (C)</td><td>0.2</td><td>6.0</td></tr><tr><td>string_copy (E)</td><td>2.6</td><td>-</td><td>split_vc.1 (C)</td><td>3.1</td><td>3.2</td><td>test0 (E)</td><td>-</td><td>13.0</td></tr><tr><td>substring1 (E)</td><td>0.3</td><td>0.7</td><td>split_vc.2 (C)</td><td>2.2</td><td>2.4</td><td>test0.optim (E)</td><td>0.4</td><td>2.7</td></tr><tr><td>substring (E)</td><td>1.3</td><td>0.7</td><td>split_vc.3 (C)</td><td>2.1</td><td>0.6</td><td>test1.optim (C)</td><td>0.4</td><td>10.7</td></tr><tr><td colspan="3"><b>(b) Examples from L2CA [2]</b></td><td>split_vc.1 (E)</td><td>19.0</td><td>2.3</td><td>test1.optim (E)</td><td>0.9</td><td>8.3</td></tr><tr><td>bubblesort (E)</td><td>9.6</td><td>0.6</td><td colspan="3"><b>(e) NECLA benchmarks</b></td><td>test2_1.optim (E)</td><td>0.9</td><td>5.9</td></tr><tr><td>insdel (E)</td><td>0.1</td><td>0.1</td><td>blast (C)</td><td>0.2</td><td>3.3</td><td>test2_2.optim (E)</td><td>1.8</td><td>7.7</td></tr><tr><td>insertsort (E)</td><td>1.4</td><td>0.6</td><td>inf1 (E)</td><td>0.1</td><td>1.4</td><td>test2.optim (C)</td><td>5.2</td><td>46.0</td></tr><tr><td>listcounter (C)</td><td>0.2</td><td>-</td><td>inf4 (E)</td><td>0.6</td><td>4.8</td><td>wrpc.manual (C)</td><td>2.3</td><td>1.8</td></tr><tr><td>listcounter (E)</td><td>0.2</td><td>0.3</td><td>inf6 (C)</td><td>0.0</td><td>3.0</td><td>wrpc (E)</td><td>-</td><td>14.7</td></tr><tr><td>listreversal (C)</td><td>3.1</td><td>0.4</td><td>inf8 (C)</td><td>0.2</td><td>4.7</td><td>wrpc.optim (E)</td><td>-</td><td>3.7</td></tr><tr><td>listreversal (E)</td><td>0.4</td><td>0.6</td><td colspan="3"></td><td colspan="3"></td></tr><tr><td>mergesort (E)</td><td>0.8</td><td>0.6</td><td colspan="3"></td><td colspan="3"></td></tr><tr><td>selectionsort (E)</td><td>0.9</td><td>0.3</td><td colspan="3"></td><td colspan="3"></td></tr></tbody></table>

## References

1. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In *FMCAD*, 2009.

2. A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In *CAV*, pages 517–531, 2006.

3. M. Bozga, P. Habermehl, R. Iosif, F. Konečný, and T. Vojnar. Automatic verification of integer array programs. In *CAV*, pages 157–172, 2009.

4. M. Bozga, R. Iosif, and F. Konečný. Fast acceleration of ultimately periodic relations. In *CAV*, pages 227–242, 2010.

5. A. Brillout, D. Kroening, P. Rümmer, and T. Wahl. An interpolating sequent calculus for quantifier-free Presburger arithmetic. In *IJCAR*, LNCS. Springer, 2010.

6. P. Ganty. Personal communication.

7. P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. *CoRR*, abs/1011.0551, 2010.

8. P. Habermehl, R. Iosif, A. Rogalewicz, and T. Vojnar. Proving termination of tree manipulating programs. In *ATVA*, pages 145–161, 2007.

9. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In *POPL*, pages 232–244. ACM, 2004.
10. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In *POPL*, 2002.

11. R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In *TACAS*, pages 459–473, 2006.

12. M. Minsky. *Computation: Finite and Infinite Machines*. Prentice-Hall, 1967.

13. P. Rümmer. A constraint sequent calculus for first-order logic with linear integer arithmetic. In *LPAR*, volume 5330 of *LNCS*, pages 274–289. Springer, 2008.

14. A. Smrcka and T. Vojnar. Verifying parametrised hardware designs via counter automata. In *Haifa Verification Conference*, pages 51–68, 2007.

## A Demonstration of Flata on the Running Example

Flata verifies the program in Figure 1(a) by computing its transfer function. The method is similar to the classical conversion of finite automata into regular expressions. We start by eliminating control states in Figure 1(b) which have no self-loop. Each such elimination requires to compose all incoming with all outgoing edge relations. Figure 3(a) shows the result after elimination of control states $l_1, l_2, l_4, l_5, l_6$, and $l_7$.

Next, we eliminate control states with self-loops. Each such elimination requires the computation of the transitive and reflexive closure of a (possibly disjunctive) relation (one disjunct for each self-loop relation). For this, we apply a semi-algorithm which is based on the algorithm from [4] computing transitive and reflexive closure of difference bounds and octagonal relations. When successful, we replace the loop with meta-transitions labeled with the computed closure. Elimination of $l_3$ in Figure 3(a) yields meta-transitions shown in Figure 3(b). Finally, we eliminate $l_3$ and $l'_3$, now without self-loops, which gives an inconsistent transfer function in Figure 3(c), thus proving correctness of the program.

<figure><img src="image_2.png" /><figcaption>**Fig. 3.** Deciding Safety by Elimination of Control Locations</figcaption></figure>
## B Demonstration of Eldarica on the Running Example

<figure><img src="image_3.png" /><figcaption>Fig. 4. Abstract reachability tree for blast.nts</figcaption></figure>

## C Example for Interpolation

As an example for interpolation, consider the infeasible path $l_0, l_1, l_2, l_3, l_6, l_7, err$ from our example program in Figure 1. By converting the statements and guards into a formula, Eldarica extracts the following path constraint:

$$ \underbrace{i_0 = 0 \land j_0 = 0 \land i_1 \ge 0 \land j_1 \ge 0 \land x_0 = i_1 \land y_0 = j_1 \land x_0 =}_{\phi(i_0, j_0, i_1, j_1, x_0, y_0)} 0 \land \underbrace{i_1 = j_1 \land x_0 \ne y_0}_{\psi(i_1, j_1, x_0, y_0)} $$

Princess derives the inconsistency of constraints like this by linear combination of the equations, as shown in Figure 5, forming the unsatisfiable consequence $0 \ne 0$. For
the given partitioning of the constraint into $\phi(i_0, j_0, i_1, j_1, x_0, y_0)$, $\psi(i_1, j_1, x_0, y_0)$, an interpolant can be computed by projecting this linear combination to the equations originating from the left partition:

$$I(i_1, j_1, x_0, y_0) \equiv -1 \cdot (x_0 - i_1 = 0) + 1 \cdot (y_0 - j_1 = 0) \equiv (y_0 - x_0 + i_1 - j_1 = 0)$$

The resulting predicate, $i_1 - j_1 = x_0 - y_0$, enables Eldarica to refine the abstract reachability tree and construct an inductive invariant for the loop in the example program, proving its safety.

<figure><img src="image_4.png" /><figcaption>Fig. 5. Proof about path constraints. All atoms are normalised to have right-hand side 0.</figcaption></figure>