**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## SV-COMP 2019

## **CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker (Competition Contribution)**

Kareem Khazem1(B) and Michael Tautschnig2

1 University College London, London, UK<EMAIL_ADDRESS>2 Queen Mary University of London, London, UK

**Abstract.** We gave CBMC the ability to explore and model check single program paths, as opposed to its default whole-program model-checking behaviour. This means that CBMC, when invoked with the --paths flag, symbolically executes one program path at a time—saving unexplored paths for later—and attempts to prove properties for only that path. By doing this repeatedly for each path that CBMC encounters, CBMC can detect property violations in a scalable and incremental way.

Implementing single-path exploration raises the question of which order the paths should be explored in. Our implementation makes it easy for researchers to implement and investigate alternative path exploration strategies. Our competition contribution uses a breadth-first strategy, where diverging paths are each pushed onto a queue at program decision points, and the path to explore next is gotten by dequeueing the oldest path to have been added.

## **1 Overview**

CBMC Path is an extension to the C Bounded Model Checker. The original CBMC tool was first described in [1] and is also competing in this year's SV-COMP (as previously described in [3]). CBMC symbolically executes C programs up to a user-defined loop unrolling bound. It generates a bit-precise encoding of the unrolled program, annotated with assertions that are the negation of properties the user wishes to verify. Such an encoding is satisfiable if the original program violates the properties. Thus, CBMC can be used to demonstrate that bugs occur when the program is run up to the unwinding bound for some input.

The original CBMC tool generates a single formula describing the disjunction of all program paths, dispatching this entire formula off to a SAT solver. The solver thus decides whether a bug exists at any point in the entire program. In contrast, CBMC Path dispatches the formula for a *single program path* to the SAT solver, checking whether that path violates any properties before continuing to execute and dispatch subsequent program paths. As with CBMC, the SAT solver used in CBMC Path for SV-COMP is MiniSat 2.2.0 [2].

c The Author(s) 2019 D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 199–203, 2019. https://doi.org/10.1007/978-3-030-17502-3\_13

K. Khazem—Juror.

The intermediate representation that CBMC uses has no control-flow structures. Instead, GOTO statements explicitly define control flow. Furthermore, all functions in the intermediate representation have a single return point, at the end of the function. Thus, program paths that diverge—either due to an explicit conditional in the original code or an unrolled loop—eventually reunite at a later point in code. The treatment of these join points is an important difference between CBMC and CBMC Path.

CBMC Path is merged into the main CBMC codebase; users activate it by passing the --paths flag to CBMC in addition to the other options that they wish to use. Since it is a fairly focussed change to the codebase, we describe only the aspects that differ from CBMC's default mode in this report.

## **2 Architecture**

The changes that CBMC Path makes to the original codebase are confined to the symbolic execution phase. There are three main changes, illustrated in Fig. 1:

Program paths are thus pushed to and popped from the worklist until one of the paths has been executed to the end of the program; at this point, the toplevel code dispatches its formula to the SAT solver, before continuing to execute the remaining paths.

The decision of which path should be resumed can be expressed as a listpopping strategy. We have so far implemented the last-in, first-out (LIFO) and first-in, first-out (FIFO) disciplines. LIFO explores the program depth-first, completing a single path before starting to explore any others; this strategy uses memory efficiently (since only a single full path is maintained in memory), but takes far longer to cover a variety of program paths. FIFO expands the exploredinstruction frontier of all program paths in a round-robin manner; this achieves excellent coverage at the (considerable) expense of keeping all paths in memory until each of them reaches the end of the program. The user can choose the strategy as an argument to the --paths option. For SV-COMP, we chose to use FIFO for all benchmarks, since the modest size of the benchmarks means that memory use was rarely a problem. The strategy system is designed to be easily extensible to encourage researchers to experiment with the different trade-offs of more sophisticated path-popping strategies.

### **3 Motivation, Strengths, and Weaknesses**

CBMC Path shares many of the strengths and weaknesses that CBMC has compared to other tools, which are discussed in the CBMC system report. In this section, we focus on a comparison with CBMC.

CBMC Path is aimed at users wishing to discover bugs quickly and efficiently, while being not so suited to proving program correctness. By only modelchecking individual program paths, each SAT solver call returns much more quickly, ensuring that bugs along those paths are discovered without having to wait for the rest of the program to be encoded and checked. In addition, CBMC Path can be parsimonious in its memory usage, since the formulas dispatched to the solver are much smaller. These qualities make CBMC Path complementary to whole-program bug-finding or correctness-proving tools. The intended use-case is that CBMC Path is used to quickly find bugs of the low-hanging fruit variety, so that users can avoid model-checking the entire program only to discover an error residing a few lines into the program entry-point.

The overhead of saving and resuming paths, and of multiple calls to the SAT solver, means that CBMC Path will always take significantly longer to check

```
1 if(x > y)
2 GOTO 3;
3 GOTO 2;
4 3: ret = 1;
5 GOTO 1;
6 2: ret = 0;
7 1: return;
```
**Fig. 1.** The program above (in CBMC's intermediate representation) illustrates the difference between CBMC's and CBMC Path's exploration strategies. CBMC executes all seven lines. At the join point (line 7), CBMC creates a disjunction representing both paths. In contrast, at line 1, CBMC Path pauses symbolic execution and saves two paths onto the top-level worklist: one path whose program counter is line 3, and another whose program counter is line 4. The top-level workloop then chooses a path from the worklist to resume executing.

an entire program than CBMC does. Proving absence of property violations always requires checking the entire program, so CBMC is expected to outperform CBMC Path on most SV-COMP benchmarks. On the other hand, CBMC Path usually has a lower maximum memory use than CBMC when using the LIFO strategy, since both the in-memory symbolic state and the formulas dispatched to the solver are smaller at all times. This means that CBMC Path can still be useful for proving correctness, specifically when used on large programs that require more-than-available system memory under CBMC. CBMC Path is most useful when used for finding bugs, since it will often find a property violation before CBMC has had a chance to fully explore the program. In addition, the user experience is often more encouraging using CBMC Path, since results are displayed incrementally. This is an important contrast to tools which terminate due to memory exhaustion before displaying any results at all. We view CBMC Path as complimentary to CBMC, and hope that developers use them both to their respective strengths.

This year (CBMC Path's SV-COMP debut), CBMC outperformed CBMC Path on most benchmarks. For small SV-COMP benchmarks, the time that CBMC spends in the solver for the entire program is less than the path pushing and popping overhead. We hope to introduce more sophisticated path strategies that will mitigate this overhead for future competitions.

## **4 Tool Setup**

The competition submission is based on CBMC version 5.10, with additional patches. The archive of the competition binary is available at https://gitlab. com/sosy-lab/sv-comp/archives-2019/raw/svcomp19/2019/cbmc-path.zip.

To process a benchmark FOO.c (with properties in FOO.prp), the wrapper cbmc-path.py should be invoked as follows:

```
cbmc - path.py --graphml -cex witness.cex \
             --propertyfile FOO.prp --32 FOO.c
```
for all categories with a 32-bit memory model; for those with a 64-bit memory model, --32 should be replaced by --64.

*Participation.* CBMC Path competes in all categories.

*Output.* The last line of output produced by cbmc is one of TRUE, FALSE, FALSE(no-overflow), FALSE(valid-free), FALSE(valid-deref), or FALSE(validmemtrack). Absence of such a final line is treated as UNKNOWN by the wrapper script.

## **5 Software Project**

CBMC Path is fully merged into the original CBMC codebase. It is maintained by Daniel Kroening with patches supplied by the community. It is made publicly available under a BSD-style license. The source code and binaries for popular platforms are available at http://www.cprover.org/cbmc.

**Acknowledgements.** We would like to thank the reviewers for their feedback and Mark R. Tuttle for his assistance with this work.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Extending DIVINE with Symbolic Verification Using SMT (Competition Contribution)**

Henrich Lauko(B), Vladim´ır Still, Petr Roˇ ˇ ckai, and Jiˇr´ı Barnat

Faculty of Informatics, Masaryk University, Brno, Czech Republic<EMAIL_ADDRESS><EMAIL_ADDRESS>
**Abstract.** DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.

### **1 Verification Approach and Software Architecture**

DIVINE is an explicit-state model checker primarily designed to detect bugs in multithreaded programs [6]. Testing of multithreaded programs is a known hard problem because of nondeterminism in the execution caused by thread interleavings. To deal with control flow nondeterminism, DIVINE exhaustively explores all relevant executions of the multithreaded program. Unfortunately, this explicit approach fails to deal with data nondeterminism caused by communication with the environment. In order to verify a program with inputs, DIVINE would need to examine all the possible inputs of the program. This would cause enormous state-space explosion and would be unmanageable in reasonable time and space.

The traditional way to cope with input values during verification is to represent them symbolically – i.e., to perform symbolic execution on the program. In DIVINE it would be sufficient to extend the LLVM interpreter to work with input values symbolically and adapt the exploration algorithm to work with symbolic states, similarly as other tools do [2,3,5]. However, this would make the core of the verification procedure more complicated and possibly slow it

This work has been partially supported by the Czech Science Foundation grant No. 18- 02177S and by Red Hat, Inc.

H. Lauko—SV-COMP jury member.

c The Author(s) 2019

D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 204–208, 2019. https://doi.org/10.1007/978-3-030-17502-3\_14

down, introduce bugs and/or reduce maintainability and extensibility. Hence, we have decided to shift the responsibility for symbolic values from the verifier to the verified program [4]. Instead of (re-)interpreting instructions symbolically, we translate symbolic instructions into equivalent explicit code which performs the computation symbolically. The transformation performs a dependency analysis on symbolic values of the program and translates symbolic instructions. By providing a set of symbolic operations as a library, we obtain a program that manipulates symbolic values. The method is further described in Fig. 1.

**Fig. 1.** Comparison of interpretation-based approach and compilation-based approaches. All manipulations of symbolic values are denoted by red color. In both cases, the virtual machine generates transitions in the state space and passes them to the model checker (MC), which performs safety analysis. In the compilationbased approach, symbolic operations are instrumented into the program, while in the interpretation-based one, they are the responsibility of the VM. (Color figure online)

In order to maintain efficiency we do not transform the entire program, but only the parts that might come into contact with symbolic values. As shown in Fig. 2, the program is analyzed starting from input points, and all downstream operations are augmented (s add, s eq), but concrete computation remains unchanged (fun). The transformed program uses a special operation called lift, which takes a concrete value and returns a symbolic one. The result of lifting \* represents an arbitrary input value.

In comparison to standard programs, a program with symbolic values might not have deterministic control flow. When a program contains a branch which depends on a symbolic value, both outcomes might be possible.1 To capture such behavior in the transformed program, we introduce a nondeterministic choice and execute both branches. We take advantage of the fact that DIVINE is already capable of handling nondeterminism. Further, in the taken path we constrain values by extending a path condition (see Fig. 3).

1 Given a symbolic value x and a branch with condition x<5, the condition can be both true and false. The program makes a nondeterministic choice and extends the path condition with *x <* 5 or *x* ≥ 5 respectively.

**Fig. 2.** Transformation to the program working with symbolic values (right).

**Fig. 3.** The transformed program builds term trees that represent symbolic values. The boxes correspond to symbolic variables while the circles are the concrete representation of terms. Question marks denote unconstrained nullary symbols. Gray boxes represent path condition constraints.

In the program, symbolic data are represented as term trees – see Fig. 3. Exploring the state space, DIVINE extracts term trees from program states in the model checking algorithm, and checks for the feasibility by querying SMT solver (Z3) for satisfiability of extracted path condition. Moreover, DIVINE needs to recognize when it has reached a repeated state. This can not be done by a simple comparison of states, because different symbolic states may represent the same set of concrete states. Hence, to check equality of states, we also utilize the SMT solver. To precisely model program arithmetic, we use the bitvector theory.

#### **2 Strengths and Weaknesses**

In comparison to bounded model checkers, DIVINE's strength is sound verification – it explores a whole state-space and uses formulae in bitvector theory to precisely represent symbolic values. However DIVINE produced a few wrong results in the competition, these should not be possible in theory and likely stem from implementation errors in the verification tool.

Our compilation-based approach has allowed us to increase modularity of the tool. It is easy to change the representation of symbolic values, the verification algorithm and even the entire verifier while preserving the transformation. Another upside is that the implementation of symbolic operations is subject to checks performed by the verifier.

On the other hand, the current implementation is only a proof of concept. Our primary goal was to show that a compilation-based approach may compete with interpretation-based approaches even though it increases the size of the verified program and therefore possibly also verification complexity. Currently, the transformation can only handle scalar values, hence verification of programs with symbolic memory is not yet possible.

### **3 Tool Setup and Configuration**

The verifier archive can be found on the SV-COMP 2019 page2 under the name DIVINE-SMT. In case the binary distribution does not work on your system, we also provide a source distribution and build instructions at https://divine.fi. muni.cz/2019/sv-comp-smt.

It is usually sufficient to run divine as follows: divine check --symbolic --svcomp TESTCASE.c. This command runs DIVINE with the SMT-based representation of symbolic data described in this paper and with SV-COMP-specific instrumentation.

For SV-COMP benchmarks, additional settings are handled by the divine-svc wrapper.3 The only option used for DIVINE-SMT is --32 for 32 bit categories. The wrapper sets DIVINE options based on the property file and the benchmark. In particular, it enables symbolic mode if any nondetermism is found, sequential mode if no threads are found, and it sets which errors should be reported based on the property file. It also generates witness files. More details can be found on the aforementioned distribution page.

DIVINE participates in all categories, but it can only produce non-unknown results for the error reachability and memory safety categories.

### **4 Software Project and Contributors**

The project home page is https://divine.fi.muni.cz. Many people have contributed to DIVINE, including Petr Roˇckai, Henrich Lauko and Vladim´ır Still. ˇ DIVINE is open source software distributed under the ISC license.

### **References**

2 https://sv-comp.sosy-lab.org/2019/systems.php.

3 To be found in the main directory of the binary archive, or in the tools directory of the source distribution. Usage: divine-svc DIVINE BINARY PROP FILE [OPTIONS] TESTCASE.c.

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **ESBMC v6.0: Verifying C Programs Using** *k***-Induction and Invariant Inference (Competition Contribution)**

Mikhail R. Gadelha1(B), Felipe Monteiro2, Lucas Cordeiro3, and Denis Nicole4

1 SIDIA Instituto de Ciˆencia e Tecnologia, Manaus, Brazil<EMAIL_ADDRESS>2 Federal University of Amazonas, Manaus, Brazil<EMAIL_ADDRESS>3 University of Manchester, Manchester, UK<EMAIL_ADDRESS>4 University of Southampton, Southampton, UK<EMAIL_ADDRESS>
**Abstract.** ESBMC v6*.*0 employs a *k*-induction algorithm to both falsify and prove safety properties in C programs. We have developed a new interval-invariant generator that pre-processes the program, inferring invariants based on intervals and introducing them in the program as assumptions. Our experiments show that ESBMC v6*.*0 using *k*-induction can prove up to 7% more programs when the invariant generation is enabled.

## **1 Overview**

The k-induction algorithm is an effective verification technique implemented in various software model checkers with the goal of proving partial correctness over a large number of different programs and properties [1–3]. Typical k-inductionbased verifiers use iterative deepening and repeatedly unwind the program to produce the verification results; its incremental nature means that it always finds the smallest falsification [2]. In SV-COMP'19, we have implemented a new interval-invariant generator that runs as a pre-processing step in ESBMC [4]. In this implementation, invariants based on intervals are automatically introduced in the program as assumptions and, although the implementation has some limitations in keeping track of the relations between variables (i.e., our abstract domain is non-relational), it significantly strengthens the *k*-induction algorithm results; in particular, we have observed that the use of invariants increases the number of correct proofs by about 7% over the SV-COMP benchmarks.

M. R. Gadelha—Jury member.

### **2 Verification Approach**

ESBMC uses a *k*-induction algorithm [2] to verify and falsify properties over C programs. Let a given C program P under verification be a finite transition system M, where we define:

Note that, in our notation, termination and error are mutually exclusive: φ(s)∧ψ(s) is by construction unsatisfiable; s is a deadlock state if T(s, s )∨φ(s) is unsatisfiable.

In each step k of the k-induction algorithm, three checks are performed: the base case B(k), the forward condition F(k) and the inductive step S(k) [2]. B(k) is the standard *bounded model checking* and it is satisfiable *iff* P has a counterexample of length *k* or less:

$$B(k) = I(s\_1) \land \bigwedge\_{i=1}^{k-1} T(s\_i, s\_{i+1}) \land \bigvee\_{i=1}^k \neg \phi(s\_i). \tag{1}$$

The forward condition checks for termination, i.e. whether the completeness threshold ψ(s) must hold for the current k. If F(k) is unsatisfiable, P has terminated:

$$F(k) = I(s\_1) \land \bigwedge\_{i=1}^{k-1} T(s\_i, s\_{i+1}) \land \neg \psi(s\_k). \tag{2}$$

No safety property φ(s) is checked in F(k) as they were checked for the current *k* in the base case. Finally, the inductive condition S(k) is unsatisfiable if, whenever φ(s) holds for k unwindings, it also holds after the next unwinding of P:

$$S(k) = \exists n \in \mathbb{N}^+. \bigwedge\_{i=n}^{n+k-1} (\phi(s\_i) \land T'(s\_i, s\_{i+1})) \land \neg \phi(s\_{n+k}).\tag{3}$$

Here T (s*i*, s*i*+1) is the transition relation after havocking the loop variables [2].

Through B(k), F(k), and S(k), the *k*-induction algorithm at a given k is:

$$kind(P,k) = \begin{cases} P \text{ contains a bug,} & \text{if } B(k) \text{ is satisfiable,} \\ P \text{ is correct,} & \text{if } B(k) \lor [F(k) \land S(k)] \text{ is unsatisfiable,} \\ kind(P,k+1), & \text{otherwise.} \end{cases} \tag{4}$$

#### **2.1 Invariant Inference Based on Interval Analysis**

Our major new feature is a new interval invariant generator for integer variables; it computes for every integer variable a lower and an upper bound of possible values. These intervals are injected into the program as assumptions (constraints) to address a limitation of the *k*-induction: when trying to check S(k), the inductive step may find spurious counterexamples if the T (s*i*, s*i*+1) over-approximation is unconstrained. This is because we havoc the variables that are written in a loop, i.e. all loop variables are assigned non-deterministic values. The effect can be seen in Eq. (3): the inductive step checks if whenever φ holds for k − 1 unwindings, it also holds in the current unwinding of the system. In Eq. (3), the state space is only constrained using the properties in the program; these are (usually) not strong enough to prove program correctness.

Several authors address this problem by generating program invariants to rule out unreachable regions of the state space, either as a pre-processing step where invariants are introduced in the program before verification [3], or during the verification itself [1,5]. Similarly to Rocha et al. [3], we perform a static analysis prior to loop unwinding and (over-)estimate the range that a variable can assume. In contrast to Rocha et al., we do not rely on external tools to infer polyhedral constraints (e.g., ax + by ≤ c, where a, b, and c are constants and x and y are variables) over C programs. Instead, we implement a "rectangular" invariant generation based on interval analysis (e.g. a ≤ x ≤ b) as a pre-processing step of the verification, i.e., before the program is symbolically executed and the resulting formulae are checked by an SMT solver.

Here we use the abstract-interpretation component from CPROVER [6]. This implements an abstract domain based on expressions over intervals; these constraints associate each variable with an upper and lower bound. The algorithm starts by assuming an unbounded interval for each variable in the program and follows the reachable instructions from the main function while updates the intervals, merging them if necessary. When loops are found, an widening operation is applied, in order to accelerate the generation process [7].

Our tool generates new invariants ϕ(s*n*) and changes Eq. (3) to use them as assumptions during verification, such that the new inductive step is defined as:

$$S'(k) = \exists n \in \mathbb{N}^+ . \varphi(s\_n) \land \bigwedge\_{i=n}^{n+k-1} (\phi(s\_i) \land T'(s\_i, s\_{i+1})) \land \neg \phi(s\_{n+k}).\tag{5}$$

The *k*-induction algorithm of Eq. (4) now uses the inductive step from Eq. (5) to participate in all categories with C programs of SV-COMP'19.

#### **3 Strengths and Weaknesses**

We have observed that the use of invariants increases the number of correct proofs in ESBMC by about 7%. This, however, comes at a cost: due to bugs in the invariant generator, the number of incorrect proofs is trebled if these invariants are used. In particular, we do not track intervals of variables changed through pointers and nor if the intervals are defined in terms of other variables. For this we would need a relational analysis that can keep track of relations between variables. As a result, with the interval invariants enabled, ESBMC becomes a (better) *bug-finding* tool rather than one delivering proofs of guaranteed soundness.

In SV-COMP'19, ESBMC correctly claims 3556 benchmarks correct and finds existing errors in 1753. Sadly, it also finds unexpected errors for 14 benchmarks and fails to find the expected errors in another 41, which impacts its overall performance. The failures are mostly concentrated in the MemSafety and ConcurrencySafety categories and are mainly due to: (1) our non-relational abstract domain, (2) an internal bug in ESBMC (since corrected) which did not track variables going out of scope, and (3) an incomplete modelling of some *pthread* functions. ESBMC's performance has improved greatly since SV-COMP'18 (v4.60): the number of errors detected has increased by 36% and the number of correct-true results increased by 32%. The biggest improvements are reflected in the categories ReachSafety and FalsificationOverall.

## **4 Tool Setup and Configuration**

In order to run our esbmc-wrapper.py script1, one must set the architecture (*i.e.*, 32 or 64-bit), the competition strategy (*k*-induction, falsification or incremental BMC), the property file path, and the benchmark path, as:

$$\begin{array}{c} \mathsf{isbmc-wrapped} \cdot \mathsf{p} \quad \{\mathsf{-h}\} \quad \{\mathsf{-a}\ \{\mathsf{32}, \mathsf{64}\}\} \quad \{\mathsf{-p} \text{ PROBERTY}\_{\mathsf{F}}\} \\ \mathsf{[-s \{\mathsf{k}\} \text{ducttion}, \mathsf{f} \text{alsi}, \mathsf{incr}\}] \\ \mathsf{[bencchmark]} \end{array}$$

where -a sets the architecture, -p sets the property file path, and -s sets the strategy, in this case, kinduction for *k*-induction.

Internally, by choosing the *k*-induction strategy, the following options are set for every property when executing ESBMC-kind: --no-div-by-zero-check, which disables the division by zero check (required by SV-COMP); --k-induction, which enables the *k*-induction; --floatbv, which enables floating-point SMT encoding; --unlimited-k-steps, which removes the upper limit of iteration steps in the *k*-induction algorithm; --witness-output, which sets the witness output path; --force-malloc-success, which sets that all dynamic allocations succeed (also an SV-COMP requirement); and --interval-analysis, which enables the invariant generation. In addition, ESBMC-kind sets further options depending on the property that needs to be checked: --no-pointer-check and --no-bounds-check for reachability verification; --memory-leak-check for memory verification; and --overflow-check for overflow verification. The Benchexec tool info module is named esbmc.py and the benchmark definition file is esbmc-kind.xml. For SV-COMP'19, ESBMCkind uses Boolector v2.4.1 [8] and competes in all categories with C programs.

## **5 Software Project**

The ESBMC source code is available for downloading at https://github.com/ esbmc/esbmc, while self-contained binaries for ESBMC v6.0 64-bit can be

1 https://gitlab.com/sosy-lab/sv-comp/archives-2019/blob/master/2019/esbmc-kind .zip.

downloaded from https://github.com/esbmc/esbmc/releases. ESBMC is publicly available under the terms of the Apache License 2.0. Instructions for building ESBMC from source are given in the file BUILDING (including the description of all dependencies). ESBMC is a joint project with the Federal University of Amazonas (Brazil), University of Southampton (UK), University of Manchester (UK), and University of Stellenbosch (South Africa).

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **JayHorn: A Java Model Checker (Competition Contribution)**

Temesghen Kahsai1, Philipp R¨ummer2(B) , and Martin Sch¨af3

> The University of Iowa, Iowa City, USA Uppsala University, Uppsala, Sweden<EMAIL_ADDRESS>SRI International, Menlo Park, USA

**Abstract.** JayHorn is a model checker for verifying sequential Java programs annotated with assertions expressing safety conditions. JayHorn uses the Soot library to read Java bytecode and translate it to the Jimple three-address format, then converts the Jimple code in several stages to a set of constrained Horn clauses, and solves the Horn clauses using solvers like SPACER and Eldarica. JayHorn uses a novel, invariantbased representation of heap data-structures, and is therefore particularly useful for analyzing programs with unbounded data-structures and unbounded run-time. JayHorn is open source and distributed under MIT license (https://github.com/jayhorn/jayhorn).

## **1 The JayHorn Approach**

JayHorn is a model checker for verifying the absence of assertion violations in sequential Java programs by automatically inferring program annotations that are sufficient to witness program safety. Annotations are quantifier-free formulas in first-order logic modulo relevant theories like LIA. The choice of annotations is inspired by refinement types [1] and liquid types [7], and consists of:

The sufficiency of annotations is characterized by a set of constrained Horn constraints expressing that state invariants in a method body are ensured by the method pre-condition and preserved by all statements in the method body, that methods establish their post-conditions, and that updating the fields of an object preserves the instance invariant inv\_C; more details are provided in [4]. Given the complete set of conditions on the annotations, the actual annotation inference can be carried out with the help of off-the-shelf Horn solvers, like SPACER [5], which uses a variant of PDR/IC3, and Eldarica [3], which uses CEGAR.

The representation of heap data-structures using instance invariants in general over-approximates the program behavior, since instance invariants have to hold for the possible states of *all* objects of some class (as well as all elements of encoded arrays), at *any* point during program execution, and they cannot refer to local variables or to fields of other objects. The encoding (and JayHorn) is therefore incomplete, and it is easy to construct correct Java programs that cannot be verified using any choice of annotations [4]. To prevent incorrect answers, JayHorn applies a counterexample validation step whenever the generated Horn clauses are found to be unsatisfiable (see Sect. 2).

**Fig. 1.** Architectural overview of JayHorn.

#### **2 Architecture of JayHorn (Fig. 1)**

*Program Transformations:* In its default configuration, JayHorn takes Java bytecode as input and checks if Java assert can be violated. JayHorn accepts any input that is supported by the Soot framework [8]: Java class files, Jar archives, or Android apk. For code that is not annotated with assert statements, Jay-Horn also provides an option to guard possible NullPointerExceptions, Array-IndexOutOfBoundsExceptions, and ClassCastExceptions with assertions.

Soot is used to translate Java bytecode to the simplified Jimple three-address format, followed by a set of transformations to further simplify a program, among them elimination of exception handling and implicit exceptional control-flow; replacement of switch statements by if statements; and de-virtualization of method calls in the input program. We can test the correctness (or soundness) of these steps by comparing input/output behavior of the original and transformed code. Since this step is crucial for the soundness of the overall system, we employ Randoop [6] to automate this test.

On the simplified input program, JayHorn performs one abstraction step to eliminate arrays, again implemented as a bytecode transformation in Soot. Arrays in Java are objects, so there are a few subtleties that makes it harder to handle them. For example, access to the length field of an array is not a regular field access but a special bytecode instruction. To simplify the later generation of Horn clauses, we transform arrays into real objects, and introduce a get and put method to access the array elements.

The next step is the replacement of all heap accesses with push/pull instructions that copy all fields of an object in a single step to/from local variables [4], preparing the ground for the later representation of heap using invariants. The placement of push/pull is optimized to use as few statements as possible, this way reducing the size of generated constraints, and minimizing the effect of later over-approximations.

*Horn Clause Generation:* The transformed simplified Java program is then encoded as a set of constrained Horn clauses, using uninterpreted predicates to represent the annotations from Sect. 1. The encoding is mostly standard, and follows the rules given in [2]. The push/pull instructions are replaced with assertions and assumptions of the corresponding instance invariant inv\_C [4].

In order to mitigate incompleteness due to the instance invariants, JayHorn implements number of refinements of the basic encoding, extending the set of programs that can be captured using instance invariants. *Flow-sensitive* instance invariants rely on a separate static analysis to determine which pushes a pull instruction can read from, and can this way distinguish different object states. *Vector references* enrich references with additional information about an object, for instance the dynamic type, the allocation site, or values of immutable fields.

*Counterexample Validation:* Since the encoding of programs using instance invariants over-approximates program behavior, there is a possibility of spurious assertion violations. JayHorn therefore implements a separate counterexample validation step with a precise, but bounded representation of heap (i.e., an underapproximate program encoding). This step is applied when the encoding with instance invariants leads to an inconclusive result. If neither over-approximate nor under-approximate encoding are able to infer a conclusive result, JayHorn reports UNKNOWN as overall verification result.

## **3 Weaknesses and Strengths**

*Weaknesses:* The development of JayHorn is ongoing, and at this point several key Java features are not fully supported yet, including (i) strings; (ii) enums; (iii) bounded integer data-types; (iv) floating-point data-types; (v) reflection and dynamic loading; (vi) concurrency. The JayHorn model of the Java API is rudimentary, so that JayHorn assumes arbitrary behavior for most API functions. Some parts of JayHorn also need more optimization to reduce the run-time of the tool, in particular some of the program transformation steps. The Horn encoding could be optimized to use fewer relation symbols with smaller arity.

*Strengths:* Due to way heap is encoded, JayHorn is particularly suitable for the analysis of relatively shallow properties of programs with unbounded iteration, unbounded recursion, or unbounded heap data-structures; examples illustrating the capabilities of JayHorn are given in [4].

*SV-COMP 2019:* The mentioned features make JayHorn a relatively bad match for the Java benchmarks used in SV-COMP 2019, which are predominantly regression tests checking the correct handling of language features and of the Java string API. A large fraction of the benchmarks (the MinePump family) relies on correct handling of enums, and could therefore not be solved by JayHorn. Only a few of the SV-COMP benchmarks contain unboundedness in the form of loops, recursion, or heap data-structures.

JayHorn gave a wrong answer for two benchmarks in the competition. The program UnsatAddition02 was incorrectly classified as correct (true), since Jay-Horn assumes unbounded integers. synchronized was incorrectly reported to be incorrect (false) due to an incomplete model of the synchronized construct, JayHorn does not support concurrency yet.

The results in the competition are overall promising, but do not represent a typical application scenario of JayHorn. The JayHorn team plans to address this for 2020 by submitting further benchmarks to SV-COMP, and by completing Java support of JayHorn, in particular fully supporting strings.

### **4 Download and Use of JayHorn**

JayHorn is fully implemented in Java, and uses the libraries mentioned in Fig. 1. The version submitted to SV-COMP 2019 is JayHorn version 0.6.1 In the configuration used in the competition,2 JayHorn only applies the Horn solver Eldarica. Since Eldarica is itself implemented in Scala, this means that no native code was used in JayHorn in the competition. The Benchexec tool info module is called jayhorn.py and the benchmark definition file jayhorn.xml. JayHorn competes in the Java category.

To run JayHorn 0.6, it is enough to download the Jar file jayhorn.jar from the link below, and run it on bytecode:

```
wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/ \
  jayhorn/src/test/resources/horn-encoding/classics/UnsatMccarthy91.java
wget https://github.com/jayhorn/jayhorn/releases/download/v0.6/jayhorn.jar
mkdir tmp
javac UnsatMccarthy91.java -d tmp
java -Xss40m -Xmx3000m -jar jayhorn.jar -inline-size 10 -solution -j tmp
```
1 https://github.com/jayhorn/jayhorn/releases/tag/v0.6.

2 Java options -Xss40m -Xmx3000m, JayHorn options -inline-size 10.

**Acknowledgement.** We are grateful for contributions to JayHorn by Daniel Dietsch, Rody Kersten, Huascar Sanchez, and Valentin W¨ustholz. The development of JayHorn is funded in parts by AFRL contract No. FA8750-15-C-0010, NSF Award No. 1422705, by the Swedish Research Council (VR) under grants 2014-5484 and 2018-4727, and by the Swedish Foundation for Strategic Research (SSF) under the project WebSec (Ref. RIT17-0011).

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)**

Lucas Cordeiro1(B) , Daniel Kroening2,3 , and Peter Schrammel2,4

 University of Manchester, Manchester, UK<EMAIL_ADDRESS>Diffblue Ltd., Oxford, UK University of Oxford, Oxford, UK University of Sussex, Brighton, UK

**Abstract.** JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.

## **1 Overview**

JBMC is a bounded model checker based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), which allows the verification of Java programs [3]. JBMC inherits memory model, symbolic execution engine and SAT/SMT backends of its sibling tool CBMC [2]. In particular, JBMC consists of a frontend for parsing Java bytecode and a Java operational model (JOM), which is an exact but verification-friendly model of the standard Java libraries. Thus, JBMC supports Java bytecode and can verify programs that make use of classes, inheritance, polymorphism, arrays, bit-level operations and floatingpoint arithmetic using CBMC's verification engine.

JBMC can reason about array bound violations, unintended arithmetic overflows, and other kinds of functional and runtime errors. However, as with other bounded model checkers, JBMC is in general incomplete, i.e., can only be used to find property violations up to a given bound *k* but not to prove properties, unless we know an upper bound on the depth of the state space by checking whether all loops have been fully unrolled; this is accomplished by inserting a so-called *unwinding assertion* at the end of each loop and recursion to check for termination.

JBMC natively supports MiniSAT as its main solver to discharge verification conditions (VCs) and check for their satisfiability, but can also be used with other incremental SAT solvers such as Glucose. For SV-COMP 2019, however, JBMC

**Fig. 1.** JBMC architecture. Grey rectangles represent input and output while white rectangles represent the JBMC main verification steps.

does not use incremental bounded model checking to verify Java programs with (multiple) loops, i.e., it does not check the VCs in iteration *k* + 1 by building upon the work done for iteration *k* [5].

### **2 Architecture**

JBMC's architecture is illustrated in Fig. 1. JBMC accepts Java bytecode class files or JAR files as input together with the JOM to parse the Java bytecode and translate it into the CPROVER control-flow graph representation, which is called a GOTO program; this transformation simplifies the Java bytecode representation (e.g., replacement of *switch* and *while* by *if* and *goto* statements) as well as lowering of exceptional control flow.

The GOTO Symex component performs a symbolic execution of the program, which thus handles dynamic memory allocation, encoding of virtual method dispatch, unrolling of the loops and unfolding of recursive method calls. In particular, JBMC uses two functions that compute the constraints *C* (i.e., assumptions and variable assignments) and properties *P* (i.e., built-in and user-defined assertions); it automatically generates safety conditions that check for null dereference, array bounds errors, type cast errors and other kinds of functional and runtime errors. Both functions accumulate the control-flow predicates at each program point and use these predicates to guard both the constraints and the properties, so that they properly reflect the Java bytecode's semantics. JBMC's VC generator then derives the VCs from these; the resulting bit-vector formula (i.e., *C* ∧ ¬*P*) is then passed on to the configured SAT solver to check for satisfiability. If this formula is *satisfiable*, then JBMC produces a counterexample; otherwise, if the formula is *unsatisfiable*, then a successful verification result is reported.

#### **3 Features**

JBMC uses an abstract representation of the standard Java libraries, called the Java operational model (JOM), which consists of simplified models of the most common classes from *java.lang* and a few from *java.util*; these models remove verification-irrelevant performance optimizations (e.g., in the implementation of container classes), exploit declarative specifications (using assume statement) and functions that are built into the CPROVER framework (e.g., for array and string manipulation).

JBMC also implements a solver for strings to determine the satisfiability of a set of constraints involving strings [4]. Specifically, our string solver implements a decision procedure for string operations that are typically used by Java programs, such as concatenation, search, extract and conversions to other data types. This decision procedure uses incremental SAT solving to lazily instantiate quantifiers.

JBMC also provides API classes that allow users to define non-deterministic verification harnesses and stub functions as used in the SV-COMP benchmarks. The API1 contains such methods for primitive data-types (e.g. nondetDouble()) and *strings* (e.g. nondetString()). The API also provides an assume(*condition*) method, which advises JBMC to ignore paths that do not satisfy a user-specified condition. JBMC is able to check for array bounds, division by zero, unintended arithmetic overflows, runtime errors in Java (e.g. illegal memory access) and user-specified assertions.

Current development efforts include improving support for regular expressions, multi-threaded programs and enabling output of VCs using the SMT-LIB format to be checked by SMT solvers such as Z3, CVC4, Boolector, MathSAT and Yices.

#### **4 Strengths and Weaknesses**

JBMC does not produce any incorrect result for any of the Java verification tasks available in SV-COMP 2019 [1]; it correctly claims 139 benchmarks correct and finds existing errors in 192. However, JBMC crashes (and returns unknown) in 37 benchmarks due to time or memory exhaustion, or due to missing models of the Java standard library. JBMC can handle most Java basic features (e.g., inheritance, polymorphism and exceptions) and strings manipulations (but *regexes* are not fully supported yet). However, JBMC's concurrency support is still limited and there is no support for Java 8 lambdas, reflection and Java Native Interface (JNI). As its sibling CBMC, JBMC can only prove bounded programs unless an upper bound is known on the depth of the state space, which is not generally the case. Lastly, our JOM does not cover the entire Java standard library.

1 https://github.com/diffblue/java-models-library/blob/master/src/main/java/org/ sosy lab/sv benchmarks/Verifier.java.

**Fig. 2.** Illustrative Java code extracted from SV-COMP 2019 (StringValueOf08).

## **5 Tool Setup**

The competition submission is based on JBMC version 5.10.2 For the competition, JBMC is called from a wrapper script.3 The wrapper script compiles the .java source files in the given benchmark directories and then invokes the jbmc binary repeatedly with increasing values for the unwinding bound until the property has been refuted (answering false) or the program has been fully unwound without finding a property violation (answering true). See the wrapper script for the relevant command line options given to JBMC. As an example, we can run the JBMC wrapper script to check for a reachability property in the program shown in Fig. 2 by executing the following command:

```
./jbmc --propertyfile <path-to-sv-benchmarks>/properties/assert.prp
   <path-to-sv-benchmarks>/java/jbmc-regression/StringValueOf08
```
where assert.prp indicates the specification to be verified for StringValueOf08. Note that this program invokes in line 4 a non-deterministic method (*Verifier.nondetString();*) to produce an arbitrary string value; this method is provided by SV-COMP in org.sosy lab.sv benchmarks.Verifier. The JOM (core-models.jar) is also part of the submission archive. If a verification task uses a Java library method that is not part of the JOM then the wrapper script returns unknown. The Benchexec tool info module is called jbmc.py and the benchmark definition file jbmc.xml. The competition submission of JBMC uses MiniSAT 2.2.1 as SAT backend. JBMC competes in the Java category.

## **6 Software Project**

JBMC is maintained by Peter Schrammel together with numerous contributors4 from the community. It is publicly available under a BSD-style license. The source code is available at http://www.github.com/diffblue/cbmc in the jbmc directory. Instructions for building JBMC from source are given in the file COMPILING.md.

2 Executable available at https://gitlab.com/sosy-lab/sv-comp/archives/tags/svco mp19.

3 Can be built from https://github.com/diffblue/cprover-sv-comp/tree/svcomp19.

4 https://github.com/diffblue/cbmc/graphs/contributors.

### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Java Pathfinder at SV-COMP 2019 (Competition Contribution)**

Cyrille Artho1(B) and Willem Visser2

1 EECS, KTH Royal Institute of Technology, 100 44 Stockholm, Sweden<EMAIL_ADDRESS>2 Department of Computer Science, University of Stellenbosch, Stellenbosch, South Africa<EMAIL_ADDRESS>https://people.kth.se/~artho/

**Abstract.** This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

**Keywords:** Java Pathfinder · Software model checking · Java program analysis

## **1 Verification Approach**

Java Pathfinder (JPF) is a framework for Java bytecode analysis [13]. At the core of the system is an explicit-state model checker [4], often just called JPF (but officially called jpf-core). This core can be extended to allow a variety of other analyses, most notably there is an extension for doing symbolic execution, called Symbolic Pathfinder [9]. Here however we focus only on the core system, i.e., on the explicit-state model checker.

JPF is a mature system with its first version released in the late 1990s. It was first open-sourced by NASA in 2004 and since around 2016 it is a community project hosted on GitHub [12]. It is based around the core algorithms for doing on-the-fly explicit state model checking, similar to SPIN. Unlike SPIN however, it does not support temporal logic property checking by itself. Instead, this functionality can be added as an extension; the core system used here only checks for uncaught exceptions (which include assertion violations).

### **2 Software Architecture**

The main architectural component of JPF is a Java virtual machine (JVM), implemented in Java. This component supports functionality for executing bytecode as well as backtracking over already executed code. Additionally a fingerprint of each state of the JVM (using hash-compaction [5]) is stored to allow

C. Artho—Jury member.

c The Author(s) 2019

D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 224–228, 2019. https://doi.org/10.1007/978-3-030-17502-3\_18

**Fig. 1.** Architecture of JPF

state-matching and to keep the analysis linear in the size of the state-space of the program being analyzed. Another optimization to allow for the efficient analysis of concurrent programs is a form of partial-order reduction that groups bytecode together in a transition as long as they cannot have any visible effect on other threads. Note that both the hash-compaction and the implementation of partialorder reduction (JPF group instructions that can only have a local effect into the same transition, but this is based on heuristics) used can cause behaviours to be missed during analysis and for this reason JPF is only a bug-finding tool, not a verification tool.

At its core, JPF treats any source of non-determinism as a choice; common choices are scheduling choices and non-deterministic choices over a range of values, e.g., whether a network is available or not [3]. In the context of SV-COMP, symbolic inputs were always treated as entirely non-deterministic choices when using jpf-core.

Java Pathfinder itself is written in Java and therefore runs on the standard JVM, called *host JVM* (see Fig. 1). The system under test (SUT) is run inside the JPF VM, and cannot directly interact with the host VM. This allows JPF to capture the full address space of the program, and revert any changes in memory when backtracking the state of the SUT during the state space search. However, this approach cannot handle native methods, which execute unmanaged code (written in C or C++) that is not supervised by JPF. Changes to memory by native methods, or other side effects thereof, are not visible to JPF. To overcome this limitation, JPF allows *model classes* to be defined, which replace the standard library classes with custom code. With this mechanism, a class with native methods can be replaced with a Java-based model class that does not use native code. Such model classes are fully managed by JPF. Sometimes, though, it is necessary to access native code, for example, to perform input/output. To achieve this, JPF supports *native peer classes*, which are executed directly on the host VM. This means that any built-in library functionality (such as I/O) is available to native peer classes. Furthermore, native peers have access to lowlevel data structures inside the JPF VM, and thus can read and modify the state of model classes or any other classes that are managed by the JPF VM.

Java Pathfinder is highly extensible and modular. Its VM can handle different platforms and instructions sets (such as Java bytecode and Dalvik code for Android), use different state space exploration strategies and schedulers, and also allows listeners to receive notifications of program state changes or execution actions, allowing users to build run-time monitoring algorithms on top of JPF. JPF extensions are vital to expand its capabilities, and allow it to handle features like the verification of distributed systems [7,11], generating missing native code on the fly [10], or monitor temporal-logic properties [8].

## **3 Discussion of Strengths and Weaknesses of the Approach**

As expected, JPF performed very well on examples with simple nondeterministic inputs such as Boolean parameters. In this case, the state space is small enough that an exhaustive search is easy, and there is no need to track path conditions (which are implemented by the Symbolic Pathfinder extension [9]). It is therefore also unsurprising that JPF did poorly in some cases where a constraint solver is required to analyze the full state space effectively. An example would be assert3 in the jbmc-regression suite where an error occurs when the input satisfies the constraint *i* ≥ 1000 ∧ *i* ≤ 1000. JPF will only enumerate the inputs for small ranges of values. Because the range of *i* is not directly specified, but indirectly derived through constraints, JPF does not analyze this variable and therefore misses this error. Finally, there were a few cases where JPF did not conclude its analysis due to missing model classes or native peers.

Java Pathfinder would really excel when analyzing simple to moderately complex concurrent applications, and applications using advanced functionality like input/output and network communication. In the 2019 benchmark set, no concurrent applications were present, so JPF is not fully utilized in this preliminary evaluation. The addition of networked applications would require additional configuration information, so it is therefore not clear how soon the benchmark suite can be extended with such additional, realistic applications. Examples that have been successfully verified by JPF in the past include a WebDAV client [2], and scp client [6], and HTTP servers [1,7].

### **4 Tool Setup and Configuration**

Java Pathfinder is available on GitHub [12]; the submitted compiled version is archived under https://gitlab.com/sosy-lab/SV-COMP/archives-2019/blob/ master/2019/jpf.zip.

Java Pathfinder (jpf-core) has no external dependencies; JUnit is necessary to run the unit tests, but not to build and use jpf-core.

JPF is compiled with ./gradlew build.

We used the default values for all options, except that cg.enumerate random was changed to true from the default configuration, because this option forces JPF to explore all possible values for random choices.1 This setting was necessary

1 JPF will explore all outcomes for Boolean choices, and a set of predefined corner cases for choices on integers.

to enable JPF to explore non-deterministic inputs. It is not enabled by default because JPF is normally used to analyze concurrency.

JPF participated in all Java benchmarks.

## **5 Software Project and Contributors**

The project is managed by the Java Pathfinder group. Contact person is Cyrille Artho (artho@kth.se). JPF is available under the Apache License, version 2.0 and hosted on GitHub [12].

**Acknowledgements.** We thank all contributors who have participated in the development of JPF over the last 20 years.

We would also like to thank Peter Schrammel and Dirk Beyer for their support, and for providing the scripts and configuration files for the competition.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **PeSCo: Predicting Sequential Combinations of Verifiers (Competition Contribution)**

Cedric Richter(B) and Heike Wehrheim

Department of Computer Science, Paderborn University, Paderborn, Germany<EMAIL_ADDRESS><EMAIL_ADDRESS>
**Abstract.** PeSCo is a tool for predicting a (likely best) sequential combination of verifiers on a given verification task and then running it. The approach is based on machine learning, more precisely on learning *rankings* of verifiers on verification tasks (where the ordering of verifiers is based on the SV-COMP scoring schema). The learning part employs Support Vector Machines; as base verifiers we use CPAchecker in 6 different configurations.

## **1 Verification Approach**

Composing verification techniques in sequence has in the past been a promising approach in the annual software verification competition SV-COMP. Especially in 20181, the software verification framework CPAchecker [3], using a composition of analyses, was able to outperform competitors in category ReachSafety. However, the analysis sequence is often predefined and fixed. In other words, a problem instance might pass through a sequence of unsuccessful verification configurations until it is processed by the right technique or exceeds a time limit.

Our competition contribution utilizes the sequential setting of CPAchecker (more precisely, of CPA-Seq), but *predicts* the order of verification tools viz. configurations. For this, we applied an extension of our rank prediction approach introduced in [7]. Basically, for a given verification task we predict an ordering of CPAchecker configurations, and then sequentially run these configurations. Configurations are ordered with respect to their (likely) performance on the verification task.

The prediction employs machine learning. For the learning, we extract *features* of verification tasks via an encoding of programs as graphs combining concepts of control-flow and program dependence graphs with abstract syntax trees. Features represent certain graph substructures of programs, where the depth of substructures considered is configurable.

1 sv-comp.sosy-lab.org/2018/results/results-verified/.

C. Richter—Jury member.

c The Author(s) 2019

D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 229–233, 2019. https://doi.org/10.1007/978-3-030-17502-3\_19

To obtain the execution order for a new problem instance, the *Ranking by pairwise comparison* (RPC) [9] framework is employed utilizing *kernelized Support Vector Machines* (SVM) [11] as base learners. By employing SVMs, we are able to choose a kernel function2 (similar to Weisfeiler-Lehman kernels [12]) that is specifically designed for graph substructures. However, the function proposed in [7] needed to be computed between the input instance X (the graph of a verification task) and *every* training sample Y , which can be quite costly in practice. As a consequence, we have re-implemented this approach and now compute Weisfeiler-Lehman-based features of *single* graphs. This significantly improves the performance of prediction.

### **2 Software Architecture**

Our tool contribution PeSCo embeds a Planning step in the restart algorithm employed in the verification framework CPAchecker [3]. The restart algorithm [10] is used in a sequential combination of verifiers to let the next verifier start on already computed (partial) results of previous verifiers, in particular when the previous verifier could not solve the verification problem. However, instead of executing a fixed list of verification techniques, our algorithm plans an execution order dependent on the verification task to be solved. Our approach consists of the following steps.

2 Kernels are similar to a similarity functions between feature vectors.

Despite the fact that our implementation is only dependent on Java 8, we need MathSAT 53 to run individual configurations. Furthermore, parser frontend for C programs are used according to CPAchecker.

**Fig. 1.** Architecture of PeSCo implemented within CPAchecker. The dotted box represent the Restart Algorithm enhanced by our rank prediction. Hence, Analysis II receives partial results of Analysis I for a restart of the verification. The rank prediction utilizes the control flow automaton extended by data and control dependencies (PDG).

#### **3 Strengths and Weaknesses**

In contrast to traditional compositional approaches, PeSCo adapts to the given tasks. As a result, our tool is able to decrease the runtime by skipping techniques that do not fit to the given verification task. More importantly, the adaptation allows us to omit analyses which introduce failures. Consequently, PeSCo improves the number of correct results in a given time frame.

Nevertheless, learning the optimal ranking requires time and introduces uncertainty to the verification process. Experiments on 1148 tasks in *ReachSafety-ECA* show that optimal rankings on a large number of *similar* programs with *different* requirements are difficult to predict. Still, the results of SV-COMP 2019 show that PeSCo can effectively verify a number of C programs in that category.

Due to the prediction process, PeSCo is furthermore limited to the configurations that occur during training. Since we trained our predictor with the version of CPAchecker employed in SV-COMP 2018, we perform slightly worse than the improved 2019 version of CPA-Seq.

3 mathsat.fbk.eu.

## **4 Tool Setup and Configuration**

PeSCo is fully integrated in the official source code of CPAchecker. Thus, it can be downloaded as a fork: https://github.com/cedricrupb/cpachecker. We use Revision b8d6131 for the competition. To compile the tool, ant should be executed on the checkout folder. After this step, our tool requires Java 8 and MathSAT 5 as external tools. To verify a test program, CPAchecker is executed with the following command line:

```
$ scripts/cpa.sh -svcomp19-pesco -benchmark -heap 10000M -stack
   -
    → 2048k -timelimit 900s -spec prop.spc program.c
```
For programs expecting a 64 Bit model, add the parameter -64. PeSCo participates in category ReachSafety, Falsification and Overall. The corresponding specification can be found in the checkout folder under config/specification/sv-comp-reachability.spc.

## **5 Software Project and Contributors**

Being an extension of the CPAchecker project, PeSCo is developed as an open-source project by a research group from Paderborn University. Contributors were so far Mike Czech, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim. We would furthermore like to thank Eyke H¨ullermeier for machine learning expertise and his contribution to the prediction process. We aso thank the CPAchecker team for allowing us to use their tool.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## Pinaka**: Symbolic Execution Meets Incremental Solving (Competition Contribution)**

Eti Chaudhary and Saurabh Joshi(B)

Department of Computer Science and Engineering, Indian Institute of Technology Hyderabad, Kandi, India<EMAIL_ADDRESS>
**Abstract.** Many modern-day solvers offer functionality for incremental SAT solving, which preserves the state of the solver across invocations. This is beneficial when multiple, closely related SAT queries need to be fed to the solver. Pinaka is a symbolic execution engine which makes aggressive use of incremental SAT solving coupled with eager state infeasibility checks. It is built on top of the CProver/Symex framework. Pinaka supports both Breadth First Search and Depth First Search as state exploration strategies along with partial and full incremental modes. For SVCOMP 2019, Pinaka is configured to use partial incremental mode with Depth First Search strategy.

**Keywords:** Symbolic execution · Incremental solving · Software bug detection

## **1 Verification Technique**

Pinaka extends symbolic execution with incremental solving coupled with eager infeasibility checks. A pure symbolic execution [6] engine builds a logical formula representing a potential execution path using symbolic values which may then be passed on to theorem-provers/solvers. An UNSAT outcome from the solver implies that the verification condition will not be violated along that path, whereas a SAT outcome provides a scenario leading to failure of an assertion during an execution along that path. The number of paths in a program blow-up exponentially as the number of branches increases. Pinaka, being a single-path symbolic execution engine, never merges two paths (i.e., diamonds). It employs eager infeasibility checks to avoid unnecessary exploration. Rather than making queries to the solver only when a path encounters an assertion, a query is made everytime a branch is encountered to check its feasibility. Infeasible branches are not explored further. These eager checks help Pinaka tremendously in reducing its search efforts. Pinaka is further powered by incremental solving [5] offered by

c The Author(s) 2019

E. Chaudhary—Jury Member.

D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 234–238, 2019. https://doi.org/10.1007/978-3-030-17502-3\_20

many state-of-the-art solvers such as MiniSAT [3]. Incremental Solving greatly benefits our technique by reducing the overhead encountered due to eager infeasibility checks. Pinaka has Depth First Search (DFS) and Breadth First Search (BFS) as its search strategies. It offers two different modes of operation: Partial Incremental (PI) Mode and Full Incremental (FI) Mode.

In PI mode, a single solver instance is maintained along a search path. In the event that a branch is encountered, only a partial path is encoded from the current point to the previous point from which a query was made along the current path. For example, in Fig. 1, a query would be made at b1. If both s1 and s2 are feasible, s2 is put in a queue and the current solver instance is used to further explore the path starting from s1. When b2 is encountered, only the path from s1 to b2 is encoded and added in the current solver instance before making a query. If both the branches at b2 are infeasible, a new solver instance is created and a path from the initial state to another symbolic state (e.g., s2) in the queue is encoded and the path along that symbolic state is explored further. Essentially, a new solver instance is created every-time a backtrack happens. Using BFS in PI mode is very memory consuming because for every symbolic state in the queue, a corresponding solver instance is retained. Running Pinaka with this combination is not recommended.

**Fig. 1.** Branching state in a program graph

In FI mode, a single solver instance is retained throughout. In Fig. 1, if b1 → s1 is a feasible branch, a new activation variable a*b*1*s*1 is created. Let φ*b*1*b*2 be the encoding of the path from b1 to b2. When b2 is encountered, a*b*1*s*1 ⇒ φ*b*1*b*2 is added in the solver, and a*b*1*s*1 is added as an assumption to enforce the path. Since the underlying SAT solvers integrated with Pinaka do not allow *popping of a stack*, upon backtrack, ¬a*b*1*s*1 is set as an assumption to disable the constraints generated by this fragment of the path.

FI mode is beneficial when the input program does not have too many paths. Otherwise, the solver becomes quite slow over time with a large memory footprint. For a large program with too many paths, the benefit of a lower memory footprint and speed of PI mode outweighs its overhead of instantiating a new solver instance on every backtrack.

{ } Loops are handled just like branches. Consider the program fragment given in Fig. 2. Assume that along some path where (x1 = 1) ∧ (y3 = −1) the loop is encountered. Branch x1 >= 3 is infeasible along this path and will not be explored. Since x1 < 3 is feasible, it is explored further by unrolling this iteration on-the-fly. Therefore, the path will further add y3 < 0. Since it is feasible, x2 = x1 + 1 is added and feasibility of x2 < 3 will be checked. After one more unrolling x3 < 3

while(x<3) if (y < 0 ) { x=x+1; }

**Fig. 2.** Handling loops

will be found infeasible, thus guaranteeing termination of the loop along this path. Note that, along a path having y3 = 2, the loop will be non-terminating for that path. In this case, Pinaka may not terminate. Function calls, including recursion, are handled in a similar fashion by inlining a call on-the-fly. Therefore, even though Pinaka provides an option of --unwind NUM to specify an unwinding limit, it does not mandate that a loop unwinding limit is specified. If a user-given unwinding limit is not sufficient to reach an assertion violation, it declares the program as *safe*, which may be unsound. To ensure soundness, we run it without any loop unwinding limit. For *unsafe* programs, upon encountering the first assertion violation, Pinaka terminates and reports a failure. For *safe* programs, however, Pinaka terminates only if all the paths of the program are terminating.

## **2 Architecture**

Pinaka 0.1 is built upon the CProver [2]+ Symex [10] framework1. Taking a C program as input, it makes use of CProver framework APIs to convert the input C program to a GOTO program. CProver APIs further come into play for preprocessing of GOTO-programs, witness generation, transformation passes such as setting the rounding-mode for floating-point operations, handling complex data types, etc. Pinaka implements PI and FI mode and eager infeasibility checks along with BFS/DFS exploration. Apart from DFS, none of those features are present in Symex [10]. Additionally, we make use of our forked version of the Symex repository in which we fix many bugs, especially for handling recursive procedures and ternary operators. As of now Pinaka only supports some MiniSAT-like solvers (i.e., Glucose [4], MapleSAT [7]) and not SMT solvers. Once a program has been verified, a verification successful/failed outcome is generated along with the appropriate witness (Fig. 3).

**Fig. 3.** Architectural overview of Pinaka

1 Note the specific Symex version used on which Pinaka is built.

### **3 Strengths and Weaknesses**

Modulo the soundness of the CProver/Symex framework and the back-end solver, Pinaka's technique is sound. In addition, if CProver/Symex do not have any overapproximation in modeling the C constructs, then a bug reported by Pinaka would indeed be a bug.

As explained in Sect. 1, Pinaka can potentially be non-terminating if for some input value there is a non-terminating path. However, termination of verification process guarantees the termination of the underlying program (modulo the approximations introduced in modeling by CProver/Symex) *if* the program is declared *safe* by Pinaka. A notable strength of Pinaka lies in its speed. A majority of Pinaka's verification outcomes were obtained under a mere limit of 10 s. A clear display of the same can be seen in the ReachSafety-Floats category, where Pinaka came in second with 1500 s CPU time [9], as compared to other tools that share a similar score but require 4 to 10 times more CPU time.

One major weakness of the current version Pinaka is a lack of techniques for loop invariants. Even with eager infeasibility checks and incremental solving, there is still a need for more loop-directed abstraction based approaches. Furthermore, support for handling multi-dimensional arrays is still lacking.

#### **4 Tool Setup and Configuration**

Pinaka 0.1 is available for download at https://github.com/sbjoshi/Pinaka. The repository contains a description of Pinaka's working along with all the necessary configuration files required to run Pinaka SVCOMP style. All the instructions are listed in a stepwise manner in the README.md file. Although Pinaka is built on top of the CProver/Symex framework, the binary itself is sufficient and the tool does not require any additional pre-requisites. Pinaka has been tested on Ubuntu 18.04.

Pinaka 0.1 submitted for SVCOMP 2019 runs DFS in PI Mode as for SVCOMP benchmarks we found this combination the best. No loop unwinding limit was specified to retain soundness. For SVCOMP'19 [1,9] it uses Glucose-Syrup (Glucose-4.1) [4] as its solver back-end. Tool's default search strategy, i.e., DFS may be overridden by providing --bfs option. Similarly, a default of FI mode may also be overridden by providing --partial-incremental option. Other additional options may be explored from the --help menu. The set of global parameters passed to the tool are: (1) --graphml-witness: to specify the witness file to be generated, (2) --propertyfile: to specify the property file, (3) --32/--64: to define the architecture to be used. Pinaka 0.1 participated in all ReachSafety subcategories *except* ReachSafety-Sequentialized, and also participated in NoOverflows and Termination meta-categories in SVCOMP 2019.

## **5 Software Project and Contributors**

Pinaka is a result of very heavy code rewriting and refactoring of VerifOx [8] (developed by Saurabh Joshi) with a lot of feature additions and bug fixes. Pinaka is developed at Indian Institute of Technology, Hyderabad, India. It is available at https://github.com/sbjoshi/Pinaka under BSD License. The authors acknowledge the financial support from DST, India under SERB ECR 2017 grant.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Symbolic Pathfinder for SV-COMP (Competition Contribution)**

Yannic Noller1, Corina S. P˘as˘areanu2,3, Aymeric Fromherz2, Xuan-Bach D. Le2, and Willem Visser4(B)

 Humboldt-Universit¨at zu Berlin, Berlin, Germany Carnegie Mellon University Silicon Valley, Moffett Field, USA NASA Ames Research Center, Mountain View, USA Stellenbosch University, Stellenbosch, South Africa<EMAIL_ADDRESS>
**Abstract.** This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furthermore, we comment on the competition results and we outline some directions for future work.

## **1 Verification Approach**

Symbolic Pathfinder (SPF) is a program analysis tool for Java bytecode; the tool is based on *symbolic execution*. In this approach, programs are executed on symbolic inputs representing multiple concrete inputs. Values of variables are represented as numeric constraints, generated from the analysis of the code structure, i.e. conditionals and other statements in the program. These constraints are then solved using different constraint solvers (both off-the-shelf and built-in-house) to generate test inputs that are guaranteed to reach those parts of the code.

The current implementation handles the following:

SPF can also be used for probabilistic analysis by leveraging model counting over symbolic constraints [2,4], and for automated program repair [6,7]. Most recent work explores combinations of SPF with AFL-style fuzzing [8] and further differential analysis for regression problems.

## **2 Software Architecture**

SPF is described in detail in a journal article [10] (however, as it is an active project, it is being updated with new features all the time). We depict the current tool architecture in Fig. 1. The input to the tool is a Java bytecode program and a configuration file that specifies different options for analysis (as discussed below). The output is a set of test sequences that execute different paths through the code. The output also lists the errors that were found (e.g. exceptions, assert violations) together with various statistics about the analysis.

**Fig. 1.** Symbolic PathFinder overview.

Symbolic execution is implemented by a "non-standard" interpretation of bytecodes. The symbolic information is propagated via *attributes* associated with program variables, operands, etc. The analysis can start from any point in the program and it can perform mixed concrete/symbolic execution. SPF relies on jpf-core's search engine to explore different paths through the code. The default search strategy is depth-first search. State matching (as implemented in jpf-core) is usually turned off during symbolic execution.

SPF uses several constraint solvers and decision procedures, most notably Z3 and Z3bitvector, which are available from https://github.com/Z3Prover/z3. SPF implements both incremental and non-incremental constraint solving.

## **3 Discussion of Strengths and Weaknesses of the Approach**

The competition results are provided on the SV-COMP website. The results indicate that SPF outperforms the other tools in terms of correct answers (337), cpu time (1300 s) and energy (13000 J). However, SPF also reported 6 incorrect results, which penalized the overall final score. While the incorrect true results are due to the bounded nature of the analysis, the incorrect false results are due mainly to the string analysis, with the exception of one result which was due to an error in jpf-core which has since been corrected. The string solver was incorrectly specified and tested (i.e. the path to the string solver is hard coded in the current implementation but we provided no string solver for the competition).

In the future we plan to test SPF on the competition string examples using either ABC or Z3str and to robustify the implementation. We also plan to contribute to the competition by adding more interesting benchmarks, particularly related to input data structures.

## **4 Tool Setup and Configuration**

Symbolic PathFinder is available at https://github.com/SymbolicPathFinder/ jpf-symbc. It requires Java 8 and Java PathFinder, which available at https:// github.com/javapathfinder/jpf-core.

For this competition we used the version with the timestamp *Mon Nov 19 09:51:16 CET 2018*, which refers to the date when we pulled the artifacts from the GitHub repository and generated the jpf-symbc jar archive.

To run SPF, the user needs to download Symbolic PathFinder and Java PathFinder (default branches) and create a file .jpf/site.properties in the home directory. The site.properties file should contain the following lines (the users should modify to point to the location of jpf-core and jpf-symbc on their computer):

```
jpf-core = ${user.home}/workspace/jpf-core
jpf-symbc = ${user.home}/workspace/jpf-symbc
extensions = ${jpf-core},${jpf-symbc}
```
The user then creates a \*.jpf configuration file (described in detail below). For the competition we modified the SPF tool to handle the non-deterministic constructs required by the competition.

#### **4.1 Example Configuration**

We give here an example configuration that can be used to run the SPF tool; this is the default configuration, that we used in the competition. The explanation for the different options is given in parenthesis.

```
– symbolic.dp=z3bitvector (specify the decision procedure)
```

```
– symbolic.max_int=100
```

```
– symbolic.min_double=-100.0
```

```
– symbolic.max_double=100.0
```

SPF also has the option of running the constraint solving incrementally. Note however that we did not use the string solving and the incremental solving options in the competition as we did not have enough time to prepare and test those features, as we were entered late in the competition.

## **5 Software Project and Contributors**

Information about the project and contributors can be found at the project webpage: https://github.com/SymbolicPathFinder/jpf-symbc. For more information please contact the authors of this paper.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **VeriFuzz: Program Aware Fuzzing (Competition Contribution)**

Animesh Basak Chowdhury, Raveendra Kumar Medicherla(B) , and Venkatesh R

Tata Research Development and Design Centre, Pune, India<EMAIL_ADDRESS>
**Abstract.** VeriFuzz is a program aware fuzz testing tool, which combines the power of feedback-driven evolutionary fuzz testing with static analysis. VeriFuzz deploys lightweight static analysis to extract meaningful information about program behavior that can aid fuzzing based testinput generation to achieve coverage goals quickly. We use constraintsolver to generate an initial population of test-inputs. VeriFuzz could generate the maximum number of counterexamples for reachsafety category benchmarks in SV-COMP 2019 and in Test-Comp 2019 [16]. (All the terms in typewriter font are competition specific. See [15].)

### **1 Introduction**

VeriFuzz is a coverage driven automated test-input generation tool based on *greybox* fuzzing [5]. The idea of grey-box fuzzing is to use lightweight instrumentation to observe behaviors exhibited during a test run. This information is used while fuzzing for new test-inputs that might exhibit new behaviors. For VeriFuzz, the behavior of interest is code coverage. VeriFuzz relies on evolutionary algorithms to generate newer test-inputs from an initial population of test-inputs. Central to an evolutionary algorithm is the *selection* of *best-fit* candidates from a *population* and generate offspring by applying *crossover* and *mutating* operations on them. The newer offspring are checked for their *fitness* against a goal. The population evolves by adding the fit offspring to the existing population. In an automated testing, a candidate test-input plays the role of an individual in a population. The new test-inputs are generated from a selected test-input by repeatedly applying mutation operations, for example, by flipping byte at a random position. The fitness of a generated test-input is determined by the code coverage during its run [11,18].

State-of-the-art grey-box fuzzers such as afl-fuzz [19], though simple to use, have several key shortcomings. (a) The fuzzer is aware of neither the program structure nor the input structure. This leads to the generation of a large set of redundant test-inputs with respect to code coverage. (b) For programs that

R. K. Medicherla—Jury Member.

c The Author(s) 2019

D. Beyer et al. (Eds.): TACAS 2019, Part III, LNCS 11429, pp. 244–249, 2019. https://doi.org/10.1007/978-3-030-17502-3\_22

does *complex* validations on their input, the fuzzer finds it hard to generate a test-input that satisfies such validation conditions [13]. Finding a suitable initial population of test-inputs for such programs requires the analysis of validation conditions. (c) For programs with unbounded loops, the fuzzer may get *stuck* forever without generating any new test-inputs. There are several approaches proposed in the literature to address some of these shortcomings [1,7,12,13]. However, all these approaches address each concern separately.

## **2 Our Approach**

In order to alleviate the problems described in Sect. 1, our approach analyses and transforms the subject program. The analysis information is then passed to the enhanced mutation engine of afl-fuzz for fuzzing the transformed program. The following are the key steps of our approach.

**Efficient Instrumentation:** To measure the coverage due to a run on a testinput, the subject program is *instrumented*. However, instrumentation adds a significant overhead to the program execution, impacting the fuzzer's execution speed. We have optimized the instrumentation overhead by placing the probes either true or false branches of each conditional statement in the program. Our scheme is efficient to implement and preserves the coverage measure though it is sub-optimal than instrumentation schemes proposed in literature [7].

**Loop Bounding:** Certain class of programs, for example, reactive programs, during their execution, either does not terminate or crash upon reaching the *error location*1. In order to handle such non-terminating programs, our approach transforms the program loops by replacing the condition in their loop heads with a known bound. This bound is increased dynamically during the fuzzer run till it finds an input that can take program execution to an error location or the budgeted time elapses.

**Novel Initial Test Population Generation:** Grey-box fuzzers find it hard to generate test-inputs that can take program execution to cover the program blocks that are guarded by complex checks [10,13]. If the initial test-input population can take program execution through some of the complex checks, fuzzing such inputs is *likely* to generate test-inputs that can pass through other complex checks [17]. In order to create such initial test-input population, our approach first flattens the program by unrolling the loops up to a certain bound. Then, a program path is chosen that contains such complex checks and path constraints are generated along that path. The constraints are solved to create an initial test-input population.

**Program Analysis to Assist Mutation:** For programs that read input only within restricted range values, it is possible to fine-tune the fuzzer's mutation operators to choose values within this restricted ranges. In order to determine

1 Program statement where error function VERIFIER error() is called.

the ranges of input values that can reach the error locations, our approach statically determines the input value ranges of the program using *k*-path interval analysis [9]. For a given program, this analysis determines the conservative over approximate ranges of input values that may reach any given program point. We have enhanced the mutation engine of the fuzzer such that it accepts the input value ranges at the error location in the program and generates inputs that have values within the given ranges.

**Algorithmic Selection of Strategies:** All the aforementioned techniques are generic enough to use across the programs. However, in order to optimize the given resource budgets in the competition, we have selectively applied a subset of techniques to a specific class of programs. For example, loop bounding technique is applied to programs where syntactic unbounded loop structures are detected. In order to identify and map the best performing set of techniques to all benchmark programs, we have grouped them into a finite set of classes and formulated it as *multi-label classification* problem. The classifier model is developed using a non-parametric supervised learning based approach [6]. The model has been trained using nine syntactic structures of a C program and a subset of techniques as classification labels. The benchmark programs from SV-COMP 2018 [14] were used as training and validation set. We have used the decision tree classifier for this multi-label classification [2].

## **3 Tool Architecture and Flow**

Figure 1 shows the architecture of the VeriFuzz tool. It consists of a fuzzing engine and an analysis engine. The core fuzzing engine is built on top of the stateof-art grey-box fuzzer afl-fuzz v2.52b [19]. The program analysis, instrumentation and transformation components of the analysis engine are implemented using the PRISM, a TCS in-house program analysis framework [8]. The initial input generation component uses CBMC v5.10 [3] as path-constraint solver. The program classification component uses an offline trained model and scikit-learn v.0.19.2 to access the model. The implementation is in C, Java, and Python languages.

The input to the tool is a program P and a safety property φ. In the first step, the syntactic features are extracted and the class of the program is determined using a program classification module. This class information is used in subsequent steps. In the second step, the program P*i* is generated using an instrumentation and transformation module. This step also emits the transformed programs for witness generation (P*w*) and initial test-input generation modules. In the next step, the program is analysed to determine input ranges. These input ranges are used to formulate the fuzzing engine parameters F*i*. Subsequently, initial test-input population T*i* is generated using the initial input generation module. The fuzz engine is then invoked with P*i*, F*i*, and T*i* as inputs.

As a first step of the fuzzing engine, the program P*i* and a harness program that implemented VERIFIER \* functions are compiled together using gcc to generate the executable program P*e*. The core fuzzer begins with T*i* as its initial

**Fig. 1.** VeriFuzz architecture.

population, executes P*e*, and measures the coverage. A test-input from the population is selected and mutated several times to generate newer test-inputs T*g*. The program P*e* is repeatedly executed with each test-input t*g* ∈ T*g* and coverage is measured. The fitness check step compares the code coverage due run on each t*g* with the historical code coverage and determines whether t*g* should be added to the population or not. This process is repeated until the core fuzzer finds a crashing test-input t*c* that causes the program run to reach the error location or the time budget is elapsed. The t*c* and P*w* are passed to a witness generation program to generate error-witness.

#### **4 Strengths and Weaknesses**

The core strength of VeriFuzz is its ability to find a test-input that can cause the program execution to reach the error locations quickly. The tool participated both in SV-COMP and Test-Comp [16]. In SV-COMP, VeriFuzz could identify 1264 out of 1458 reachsafety FALSE benchmarks with 67 s as mean time per verification task. Whereas in Test-Comp, it could identify bugs in 592 out of 636 benchmarks. VeriFuzz could generate test-inputs that can, on an average, cover 70% branches in 1720 benchmarks.

VeriFuzz explores the concrete program paths randomly and redundantly due to its evolutionary approach. Therefore it may not always discover a test-input that cause the execution to reach an error location.

#### **5 Tool Configuration and Setup**

The VeriFuzz tool for testing SV-COMP benchmarks is available at the URL https://gitlab.com/sosy-lab/sv-comp/archives-2019/blob/master/2019/verifuzz .zip. Its Test-Comp 2019 variant is available at the URL https://gitlab.com/sosylab/test-comp/archives-2019/blob/master/2019/verifuzz.zip. The benchexec tool-info module is verifuzz.py and the benchmark description file is verifuzz.xml. To install and run the tool, follow the instructions provided in README.txt with the tool. A sample run command is as follows:

./scripts/verifuzz.py --propertyFile unreach-call.prp example.c

## **6 Software Project and Contributors**

VeriFuzz is developed by the authors at TCS Research. We would like to thank B. Chimdyalwar and S. Kumar from VeriAbs [4] team for the help in the understanding of *k*-path interval analysis.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **VIAP 1.1 (Competition Contribution)**

Pritom Rajkhowa(B) and Fangzhen Lin

Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Clear Water Bay, Kowloon, Hong Kong<EMAIL_ADDRESS>
**Abstract.** VIAP (Verifier for Integer Assignment Programs) is an automated system for verifying safety properties of procedural programs with integer assignments and loops. It is based on a translation from of a program to a set of first-order axioms with quantification over natural numbers, and currently makes use of SymPy as the algebraic simplifier and the SMT solver Z3 as the theorem prover. Our first version of the system competed at SV-COMP 2018. This paper describes VIAP 1.1, a new version that makes use of our newly developed recurrence solver. As a result, VIAP 1.1. is able to verify many programs that were out of reach for the older version VIAP 1.0.

**Keywords:** Automatic program verification · First-order logic · Mathematical induction · Recurrences · SMT · Arithmetic

## **1 Introduction**

VIAP (Verifier for Integer Assignment Programs) is an automated system for verifying safety properties of procedural programs with integer assignments and loops. It translates a given program to a set of first-order axioms with natural number quantification using an algorithm proposed by Lin [1]. An earlier version of VIAP competed at SV-COMP 2018, and is described in [2,3]. A key feature of Lin's translation is that loops are translated to a set of recurrence relations. Then, VIAP simplifies those axioms by using a Python library for symbolic computation systems, *SymPy* [4], to compute the closed-form solutions of recurrence relations. *SymPy* is equipped with function *rsolve()* to compute closed-form solution of recurrence relation. The translation of the loop body generates recurrence relations which are either simple non-conditional, conditional or mutual in nature. But *rsolve()* can find the closed form solution only for certain class of simple non-conditional recurrence relations. This motivated us to design a recurrence solver (RS) that goes beyond what the *rsolve()* function can do in *SymPy*, and integrate it with our system. The new system, VIAP 1.1, is the one that will compete at this year's SV-COMP. VIAP 1.1 continues to use *SymPy* for simplifying algebraic expressions, and the SMT solver Z3 [5] as the underlying theorem prover without ever explicitly generating loop invariants. Because of the new recurrence solver, VIAP 1.1 can solve many more benchmarks that were previously out of the reach of VIAP 1.0.

To illustrate how our system works, consider the simple program below:

```
int x=0,y=0;
while (x<100) { if (x < 50){ y++; } else { y--; } x++; }
assert(y==0);
```
With some simple simplifications, the translation outlined in [1] would generate the following axioms:

$$\begin{aligned} x\_1 &= x\_2(N), y\_1 = y\_2(N), \\ \forall n. x\_2(n+1) &= x\_2(n) + 1, x\_2(0) = 0, \\ \forall n. y\_2(n+1) &= ite(x\_2(n) < 50, y\_2(n) + 1, y\_2(n) - 1), y\_2(0) = 0, \\ \neg(x\_2(N) < 100), \forall n. n &< N \to x\_2(n) < 100. \end{aligned}$$

Here, x1 and y1 denote the output values of x and y, respectively, and x2(n) and y2(n) denote the values of x and y during the n-th iteration of the loop, respectively. The conditional expression ite(c, e1, e2) has value e1 if c holds and e2 otherwise. Also N is a natural number constant, and the last two axioms say that it is exactly the number of iterations the loop executes before exiting.

There are two recurrence relations in the above axioms. Both the recurrence relations are passed to RS. It first solves x2(n) which yields the closed-form solution x2(n) = n which can then be used to simplify the recurrence relations for y2(n) into

$$y\_2(0) = 0, \ y\_2(n+1) = i
te(n < 50, y\_2(n) + 1, y\_2(n) - 1).$$

Then RS tries to solve the above simplified conditional recurrence relations, and returns the following closed-form solution:

$$y\_2(n) = i te(0 \le n < 50, n, 50 - n).$$

After computing the closed-form solutions for x2() and y2() by RS, VIAP eliminates them, and produces the following axioms:

$$\begin{aligned} x\_1 &= N \land y\_1 = i \land (0 \le N < 50, N, 100 - N), N \ge 100), \\ \forall n. n &< N \to n < 100. \end{aligned}$$

The translation of assertion results y1 == 0. With this set of axioms, SMT solvers like Z3 can then be made to prove the assertion. Similarly, when an assertion like assert(y==1) is made to prove using above set of axioms, then Z3 will return following counterexample:

$$[y\_1 = 0, N = 100, x\_1 = 100].$$

Using this counterexample, VIAP constructs the violation witness.

## **2 VIAP Architecture**

VIAP is implemented in Python 2. VIAP has been developed in a modular fashion, and its architecture is layered into two parts:

**Translation.** Given a program P, and a language *X*, our system generates a set of first-order axioms denoted by Π*X P* that captures the changes of P on *X*. Here, a language means a set of functions and predicate symbols. For Π*X P* to be correct, *X* needs to include all program variables in P as well as any functions and predicates that can be changed by P. The axioms in the set Π*X P* are generated inductively on the structure of P. The algorithm is described in detail in [1] and an implementation is explained in [2]. The inductive cases of translations are given in the table provided in the supplementary information1. We have extended our translation programs with arrays; the extension is described in detail in [3].

**Recurrence Solver (RS).** The main objective of this module is to find closedform solutions of recurrence relations generated from the translation of the loop body. Our recurrence solver (RS)2 takes a set of recurrence relation(s) and other constraints, returns a set of closed-form solutions it found for some of the recurrences and the remaining recurrences relations and constraints simplified using the computed closed-form solutions. It uses *SymPy* [4] (V 1.1.1) as the base solver. The RS classifies input recurrence relation(s) into three major categories (1. non-conditional 2. mutual and 3. conditional recurrences relation) and applies the following corresponding sub-solver and tries to find closed form solution(s).

– The Non-Conditional Recurrence Solver (NCRS): RS applies this sub solver to the non-conditional recurrence relation(s) of the form of either

$$X(n+1) = f(X(n), n),$$

where f(x, y) is a polynomial function of x and y or

$$X(n+1) = X(n) + f(n) + A\_1 F\_1(n) + \dots + A\_k F\_k(n),$$

where f(n) is a polynomial function in n, A*i*'s are constants, and F*i*'s are function symbols.

1 https://github.com/VerifierIntegerAssignment/VIAP ARRAY/blob/master/ Document/Inductive Translation.pdf.

2 https://github.com/VerifierIntegerAssignment/recSolver.

– The Mutual Recurrence Solver (MRS): RS applies this sub solver to a set *σ* of the mutual recurrence relations where each σ ∈ *σ* is the form of

$$X\_i(n+1) = A \* (X\_1(n) + \dots + X\_h(n)) + C\_i, \qquad \text{for } 1 \le i \le h,$$

where A and C*i* are constants.

– The Conditional Recurrence Solver (CRS): RS applies this sub solver to conditional recurrence relation(s) of the form

$$X(n+1) = i te(\theta\_1, f\_1(X(n), n), ite(\theta\_2, f\_2(X(n), n) \dots, f\_{h+1}(X(n), n))),$$

where θ1, θ2,...,θ*h* are Boolean expressions, and f1(x, y), f2(x, y),..., f*h*+1(x, y) are polynomial functions of x and y.

**Instantiation:** Instantiation is one of the most important phases of the preprocessing of axioms before the resulting set of formulae is passed on an SMTsolver according to some proof strategies. The objective is to help an SMT solver like Z3 to reason with quantifiers. There are two strategies (1) Instantiating arrays and (2) Instantiating array indices applied to an array element assignment that occurs inside a loop. More details are provide in the supplementary information3.

**Proof Strategies:** As the semantics of P are precisely encoded as Π*X P* , the goal is to prove that α ∧ Π*X P* |= β, where α is a set of assumption(s) and β is the set of assertion(s) to prove. We work in a refutation-based proof schema, i.e., in order to prove that a formula is valid in a background theory T, we show that α ∧ Π*X P* ∧ ¬β is T-unsatisfiable. In VIAP, we implemented two different strategies whose details can be found in our previous work [2].

#### **3 Strength and Weaknesses**

VIAP supports user assertions, including reachability of labels in the C-code. In SV-COMP 2019, these checks are only enabled for ReachSafety-Arrays, ReachSafety-Loops and ReachSafety-Recursive sub-categories of ReachSafety category. VIAP translates a program to a set of axioms and then uses off-theshelf systems like SymPy and Z3 to prove properties about the program. The advantage (strength) of this approach comes with a clean separation between the translation (semantics) and the use of the translation in proving the properties (computation). The translation part is stable. But as more efficient provers become available, the capabilities of the system improve. This is seen in our newer version of VIAP that we entered in this year's competition: by having a more powerful system for computing closed-form solutions of recurrences, the new system becomes more efficient and can prove many properties that our

3 https://github.com/VerifierIntegerAssignment/VIAP ARRAY/blob/master/ Document/TranslatonInsRules.pdf.

previous system were not able to. However, VIAP provides little or no support for translation and reasoning about dynamic linked data structures or programs with floating points. We are working in the direction to strengthen our frontand backhand to handle all types of the program so that we can participate in all the sub-categories of ReachSafety in the future edition of SV-COMP. The SVCOMP'19 results show that VIAP can effectively verify a number C programs from those categories. VIAP came in first in the ReachSafety-Arrays and ReachSafety-Recursive sub-category. The major disadvantage of the method which translates loop body to the recurrence relation is that if they failed to find closed form solution, then they unable to find suitable invariant as a result they failed to complete the proof. When VIAP fails to come up with a closed-form solution, it falls back to simple induction using Z3. There is clearly a need of better way to do induction and we are working on it. In terms of closed-form solution, in general it is undecidable whether a recurrence has a closed-form solution or not.

## **4 Tool Setup and Configuration**

The version of VIAP (version 1.1) submitted to SV-COMP 20194 is provided as a set of binaries and libraries for Linux x86-64 architecture. The options for running the tool are:

```
./viap_tool.py --spec=SPEC INPUT
```
SPEC is the property file, and INPUT is a C file. The output of VIAP is "VIAP OUTPUT True" when the program is safe. When a counterexample is found, it outputs "VIAP OUTPUT False" and a file named errorW itness.graphml that contains the witness of error-path is generated in the VIAP root folder. If VIAP is unable find any result it outputs "UNKNOWN".

## **5 Software Project and Contributors**

VIAP is an open-source project, mainly developed by Pritom Rajkhowa and Professor Fangzhen Lin of the Hong Kong University of Science and Technology. We are grateful to the developers of Z3 and *SymPy* for making their systems available for open use.

**Acknowledgments.** We are very thankful to the anonymous reviewers for their helpful comments on an earlier version of this paper.

4 https://gitlab.com/sosy-lab/sv-comp/archives-2019/blob/master/2019/viap.zip.

### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## Author Index

Amparore, Elvio 50 Artho, Cyrille 224

Barnat, Jiří 204 Bartocci, Ezio 3, 41 Basak Chowdhury, Animesh 244 Berthomieu, Bernard 50 Beyer, Dirk 3, 133, 167 Black, Paul E. 3

Chaudhary, Eti 234 Chin, Wei-Ngan 116 Ciardo, Gianfranco 50 Cordeiro, Lucas 209, 219 Cyprian, Michal 116

Dal Zilio, Silvano 50 Durán, Francisco 93

Enea, Constantin 116 Ernst, Gidon 176

Falcone, Yliès 41 Fedyukovich, Grigory 3 Fromherz, Aymeric 239

Gadelha, Mikhail R. 209 Gallà, Francesco 50 Gao, Chong 116 Garavel, Hubert 3, 93 Giesl, Jürgen 156 Gorogiannis, Nikos 116

Hahn, Ernst Moritz 69 Hartmanns, Arnd 3, 69 Hendriks, Dennis 101 Hensel, Christian 69 Hillah, Lom Messan 50 Howar, Falk 101 Huisman, Marieke 3, 176 Hulin-Hubard, Francis 50 Iosif, Radu 116

Jasper, Marc 101 Jensen, Peter Gjøl 50 Jezequel, Loïg 50 Joshi, Saurabh 234

Kahsai, Temesghen 214 Katelaan, Jens 116 Khazem, Kareem 199 Khoo, Siau-Cheng 116 Klauck, Michaela 69 Klein, Joachim 69 Kordon, Fabrice 3, 50 Křetínský, Jan 69 Kroening, Daniel 219 Kuppens, Harco 101

Lauko, Henrich 204 Le Botlan, Didier 50 Le, Quang Loc 116 Le, Ton-Chanh 116 Le, Xuan-Bach D. 239 Lengal, Ondrej 116 Liebke, Torsten 50 Lin, Fangzhen 250

Matheja, Christoph 116 Medicherla, Raveendra Kumar 244 Meijer, Jeroen 50 Middeldorp, Aart 25 Miner, Andrew 50 Monteiro, Felipe 209 Mostowski, Wojciech 176 Mues, Malte 101 Murtovi, Alnis 101

Nagele, Julian 3, 25 Navarro Pérez, Juan A. 116 Nguyen, Thanh-Toan 116 Nicole, Denis 209

Noll, Thomas 116 Noller, Yannic 239 Parker, David 69 Păsăreanu, Corina S. 239 Paviot-Adet, Emmanuel 50 Quatmann, Tim 69 R, Venkatesh 244 Rajkhowa, Pritom 250 Reger, Giles 41 Reynolds, Andrew 116 Richter, Cedric 229 Ro čkai, Petr 204 Rogalewicz, Adam 116 Rubio, Albert 156 Ruijters, Enno 69 Rümmer, Philipp 214 Rybalchenko, Andrey 116

Sch äf, Martin 214 Schiffelers, Ramon 101 Schl üter, Maximilian 101 Schordan, Markus 101 Schrammel, Peter 219 Serban, Cristina 116 Shintani, Kiraku 25 Sighireanu, Mihaela 3 , 116 Srba, Ji ř í 50 Steffen, Bernhard 3 , 101 Steinmetz, Marcel 69 Sternagel, Christian 156 Štill, Vladimír 204 Suda, Martin 3 Sutcliffe, Geoff 3

Ta, Quang-Trung 116 Tautschnig, Michael 199 Thierry-Mieg, Yann 50

Ulbrich, Mattias 176

Vaandrager, Frits W. 101 van Dijk, Tom 50 Visser, Willem 224 , 239 Vojnar, Tomas 116

Waldmann, Johannes 156 Weber, Tjark 3 Wehrheim, Heike 229 Wolf, Karsten 50 Wu, Zhilin 116

Yamada, Akihisa 3 , 156

Zuleger, Florian 116