Infer demonstrates low analysis precision. Figures 2a and 2b illustrate a low precision across function calls (intraprocedural analysis): Both programs contain an unreachable, signed integer overflow. The only difference is the indirection in Fig. 2b due to the additional function call. Infer correctly reports Fig. 2a safe, but incorrectly reports an alarm for Fig. 2b. We assume that the intraprocedural analysis of Infer does not check whether reach\_error is reachable from the program entry. Infer-sv mitigates this issue for property unreach-call through the mentioned program transformation, but this imprecision still leads Infer to report wrong alarms across all program properties.

Infer can also show imprecision within a single function. Consider Figs. 2c and 2d: The only change between Fig. 2c and Fig. 2d is the addition of a statement in line 6, y = y + 2. This has no influence on the integer overflow in line 5, so both programs contain an overflow. Infer correctly reports the overflow for Fig. 2c, but wrongly reports Fig. 2d safe.

These imprecisions strongly reflect in the SV-COMP results of Infer, leading to many incorrect proofs and alarms.

# 3 Usage

Infer-sv requires Python 3.6 or later. Script setup.sh downloads and extracts version 1.1.0 of Infer. From the tool's directory, Infer-sv can be run with the following command:

```
./ infer - wrapper . py \
     -- data - model { ILP32 or LP64 } \
     -- property path / to / property . prp \
     -- program path / to / program . c \
```
Setting the data model is optional. Infer-sv will print the recognized property and the command line it uses to call Infer. Infer-sv prints the full output of Infer, including all warnings, and the final verification verdict on the last line. The verification verdict can be true, false, unknown or error.

# 4 Conclusion

The participation of Infer in SV-COMP allows an objective comparison with other verifiers for C. This shows that the selected analyses of Infer are very efficient, but suffer from strong imprecision on the considered benchmark tasks.

Contributors. Infer 7 is developed by Facebook and the open-source community under the MIT license, and Infer-sv 8 is developed under the Apache 2.0 license at the Software and Computational Systems Lab at LMU Munich, led by Dirk Beyer.

7 https://github.com/facebook/infer

8 https://gitlab.com/sosy-lab/software/infer-sv

Funding Statement. This work was funded in part by the Deutsche Forschungsgemeinschaft (DFG) – 418257054 (Coop).

Data Availability Statement. All data of SV-COMP 2022 are archived as described in the competition report [1] and available on the competition web site. This includes the verification tasks, results, witnesses, scripts, and instructions for reproduction. The version of our verifier as used in the competition is archived together with other participating tools [2].

#### 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.

# LART: Compiled Abstract Execution⋆ (Competition Contribution)

Henrich Lauko  ⋆⋆ and Petr Roˇckai

Faculty of Informatics, Masaryk University, Brno, Czech Republic<EMAIL_ADDRESS>
Abstract. lart – llvm abstraction and refnement tool – originates from the divine model-checker [5,7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verifcation backend but performs the verifcation natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efciency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.

Keywords: Abstract interpretation · Compilation-based abstraction · llvm · lart · divine · Formal verifcation · Symbolic execution.

# 1 Verifcation Approach and Software Architecture

As it is with many tasks in computer science, one can approach them in multiple ways, and verifcation is not an exception. In general, tools approach program analysis using an interpretation, giving them complete control over a program state and program execution but paying the cost for performance. Our tool lart challenges the task utilizing the toolset from the opposite side of the spectrum – compilation – using a technique of so-called compilation-based abstraction. The main idea of this approach is to compile nondeterministic execution directly into the executable and perform reachability analysis by its native execution. This approach is most similar to one presented in symcc [6]. Symcc performs a compilation of symbolic execution into the native binary. In contrast, we present a more general approach that allows arbitrary abstraction. Spin model checker [4] also provides a mode where the model is compiled together with a verifer to a single executable.

During the compilation, lart performs llvm-to-llvm transformation to augment instructions that can manipulate with nondeterministic values. This is

⋆ This work has been partially supported by Red Hat, Inc.

⋆⋆ Jury member representing lart at sv-comp 2022.

a purely syntactic abstraction of a program, e.g., add instruction is replaced by call to lart add. Additionally, lart provides a set of semantic libraries (abstract domains) to give meaning to abstract instruction. Each abstract domain defnes the native representation of abstract values, implements abstract instructions and transformations to and from concrete values and other domains. The tool provides multiple domains that allow analyses with various precisions, e.g., interval analysis, nullity analysis, or symbolic analysis. Finally, to allow native execution, domains are present in static libraries linked to instrumented programs under test.

In comparison to concrete programs, abstracted programs also exhibit nondeterministic control fow. To explore all possible execution paths, lart provides a confgurable runtime library. The overall architecture of compilation-based abstraction is depicted in fgure Figure 1.

The confguration used in the competition contribution employs an iterative deepening search of program paths. At each branching point of a program, the execution forks to explore all possibilities. Finally, the main process of the analysis gathers results from explored paths and notifes the user if an error is reachable. This approach eventually sufers from potential infnite loops and path explosion problem. However, it is sufcient for bug hunting or even verifcation in the case of employed overapproximative abstraction, which widens the efect of infnite loops. Also, in many simple cases, a compiler can summarize the efects of program loops, minimizing the impact of path explosion.

Fig. 1. lart architecture overview.

In order to obtain a performant result, we strive to minimize the amount of syntactic abstraction. Instrumentation achieves this by combining forward datafow analysis and Andersen alias analysis [1], tainting only those instructions that might encounter nondeterministic values, and abstracting only the tainted instructions. This analysis is entirely overapproximative and detects all possible candidates for abstraction quickly. The actual abstract computation is resolved later during execution.

However, we don't want to perform expensive abstract computation when tainted instructions do not obtain nondeterministic operands. This might occur when a C function at one point receives concrete arguments and at another call site some abstract arguments. In the former case, we would like to perform it fully concretely. While in the latter, we want to execute only the necessary amount of tainted instructions abstractly. Therefore, lart synthesizes simple dispatch routines that pick a concrete or abstract instruction depending on the operands. The dispatch routine also handles the possibility of mixing concrete and abstract operands – lifting concrete values to an abstract domain if necessary. We require that all operands of abstract instructions are in the same domain. See an example of dispatch in Figure 2.

```
__lart_value __lart_dispatch_add ( __lart_value a , __lart_value b) {
    if ( is_abstract (a) || is_abstract ( b )) {
         if (! is_abstract (a ))
              a. abstract = lift (a . concrete );
         else if (! is_abstract ( b ))
              b. abstract = lift (b . concrete );
         return domain :: add (a . abstract , b . abstract );
    }
    return a. concrete + b . concrete ;
}
```
Fig. 2. Syntactically abstracted values in lart are represented in union type of an abstract or concrete type ( lart value). The dispatch routine lifts operands to an abstract domain and resolves in which domain the instruction should be executed. Since the abstraction dispatch is purely syntactic, it can be inlined to abstracted source code and further optimized. This gives the compiler a possibility to optimize repeated checks in dispatch routines.

The runtime for native execution takes care of multiple responsibilities. First of all, it implements an execution fork when a branch is conditioned by the abstract value that results in both possibilities, e.g., when a branch is conditioned on symbolic term x < 5, both outcomes are possible. Furthermore, the runtime takes care of memory management of abstraction. To not disrupt the original program's memory layout, lart keeps all abstract data in a shadow memory. Therefore the union values presented in Figure 2 are split into two separately addressed regions – concrete program memory and abstract shadow memory. The information on whether variables hold an abstract value is also kept in the shadow memory.

#### 2 Strengths and Weaknesses

The main strength of the compilation-based abstraction is in the utilization of native runtime and compiler optimizations on abstracted code. From theory, the native execution should consistently outperform the same interpreted analysis. However, it comes at the cost of a more complex source transformation that is harder to relate to its origin. Furthermore, the overapproximative nature of the syntactic analysis produces unnecessary execution of dispatch functions when not needed. In contrast, an interpreter can compute in specifc domain without additional dispatches. Another advantage of the approach is a reusable result of syntactic abstraction that can be linked with various domains to perform analysis concurrently without repeated llvm instrumentation.

The best comparison of lart is with the divine model-checker, which uses lart's transformation and domain libraries internally, but instead of compiling to native executable, it interprets abstracted llvm ir. Results from the competition support the hypothesis that the compilation-based approach of lart outperforms divine in all reachability subcategories, except one where longer times are caused by diferent state space exploration order.

Given the simplistic runtime, abstracted binaries produced by lart lack further analysis optimizations and verifcation capabilities. Presently, the exploration algorithm only supports reachability analysis of single-threaded programs. However, we plan to support memory safety and overfow checking using sanitizers like approach.

Another goal of lart's compilation-based approach is to provide a reusable abstraction component for verifcation tools. The proof of this concept is shown on divine and now on the native mode that can be analyzed by standard programmer toolset, like debuggers or sanitizers.

### 3 Tool Setup and Confguration

The verifer archive can be found on the sv-comp 2022 [2] page under the name lart. In case the binary distribution does not work on your system, we also provide a source distribution and build instructions at https://github.com/xlauko/ lart/tree/svcomp-2022. It is sufcient to run lart using compiler wrapper script as follows: lartcc <domain> testcase.c -o abstract and then execute the abstract binary to perform the analysis.

For sv-comp contribution, lart wrapper handles additional settings and setup of workfow presented in Figure 1. The wrapper sets lart options based on the property fle and the benchmark. In particular, lart enables symbolic mode if any nondeterminism is found, and it sets which errors should be reported based on the property fle. It also generates witness fles. More details can be found on the aforementioned distribution page. Due to support limitation lart participates only in ReachSafety and DeviceDrivers categories.

### 4 Software Project and Contributors

The project home page is https://github.com/xlauko/lart. The lart is open source software distributed under the MIT license. Active contributors to the tool are listed as authors of this paper.

Data Availability Statement. All data of SV-COMP 2022 are archived as described in the competition report [2] and available on the competition web site. This includes the verifcation tasks, results, witnesses, scripts, and instructions for reproduction. The version of our verifer as used in the competition is archived together with other participating tools [3].

#### 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.

# Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding∗ (Competition Contribution)

Marek Chalupa B, Vincent Mihalkoviˇc, Anna Recht´aˇckov´a, ˇ Luk´aˇs Zaoral, and Jan Strejˇcek

Masaryk University, Brno, Czech Republic

Abstract. The development of Symbiotic 9 focused mainly on two components. One is the symbolic executor Slowbeast, which newly supports backward symbolic execution including its extension called loop folding. This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, Symbiotic 9 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of Symbiotic. We have also extended forward symbolic execution in Slowbeast with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings.

Symbiotic 9 is the Overall winner of SV-COMP 2022. Moreover, it won also the categories MemSafety and SoftwareSystems, and placed third in FalsificationOverall.

# 1 Verification Approach

Symbiotic 9 combines fast static analyses with code instrumentation and program slicing [13] to speed up the code verification. In the SV-COMP configuration of Symbiotic 9, the code verification is performed by symbolic executors, namely by Slowbeast [8] and our fork of Klee [4].

As Symbiotic works internally with llvm [10], it first compiles the given C program into llvm bitcode. The following steps depend on the verified property.

Verification of the Property unreach-call For this property, Symbiotic 9 directly slices the llvm bitcode to remove instructions that have no influence on the reachability of error calls and then run Klee with the time limit of 333 seconds. Klee is very efficient and often decides the task within this time limit. If Klee fails to decide, we parse its output and proceed according to the case of the failure. If Klee failed because the program contains threads, we

∗ This work has been supported by the Czech Science Foundation grant GA19-24397S.

B Jury member and the corresponding author<EMAIL_ADDRESS>

Table 1. The comparison of supported features of Klee (our fork and the upstream) and Slowbeast (SV-COMP 2022 and SV-COMP 2021 versions). The marks ✓/✓/✗ mean supported/partially supported/unsupported.

run Slowbeast with forward symbolic execution (SE) and the threads support turned on. If Klee failed for any other reason, we run Slowbeast with backward symbolic execution with loop folding (BSELF) [8] described later. If BSELF also fails (the current implementation supports only selected program features), we run Slowbeast with forward symbolic execution.

Note that running forward symbolic execution first with Klee and then with Slowbeast if Klee fails does make a good sense as Klee and Slowbeast support a different set of features. The main differences between these tools (and the upstream Klee and the version of Slowbeast used in Symbiotic 8) are summarized in Table 1. Row symbolic addresses indicates whether tools model the non-determinism in the placement of allocated objects (this is useful, e.g., when comparing addresses of such objects). Row incremental solving indicates whether tools can associate the state of an SMT solver to every symbolic execution state and incrementally add constraints instead of always solving formulas from the scratch. Row caching solver calls indicates whether tools can remember results of solver calls and use them later to quickly decide some other solver calls. Finally, row lazy memory indicates if the tool can create memory objects on-demand when first accessing them, without their previous allocation (it assumes that the accesses to memory are valid). This feature is crucial when we want execute a program by parts, without starting from the entry point. The meaning of the remaining rows should be clear or is explained later.

If an error is found by either tool, it is replayed on the unsliced code. If the replay succeeds, we generate a violation witness. If no error is found and the analysis was complete, we generate a correctness witness. If the program correctness was proved by Slowbeast with BSELF, we generate a witness containing the computed invariants, otherwise we generate a trivial correctness witness as we have no invariants at hand. In all other cases, Symbiotic 9 answers unknown.

Verification of Other Properties For verification of other properties than unreach-call, Symbiotic 9 uses the same workflow as Symbiotic 8 [7]. In brief, the instrumentation module marks program instructions that can potentially violate the considered property. The module employs suitable fast static analyses to identify these instructions (e.g., when checking the property no-overflow, it uses a range analysis to discover the instructions that may perform a signed integer overflow). The bitcode with marked instructions is sliced such that the arguments and the reachability of these instructions are preserved. The sliced bitcode is passed to Klee. If it discovers a property violation and then replays it on the unsliced code, we produce a violation witness. If Klee completes its analysis without any property violation found, we produce a trivial correctness witness. In all other cases, Symbiotic 9 returns unknown.

Backward Symbolic Execution with Loop Folding (BSELF) [8] Slowbeast newly implements backward symbolic execution (BSE) [9], which explores the program backward from target locations towards the initial location and incrementally computes weakest preconditions for the explored program paths. BSE is a valuable technique on its own as it precisely corresponds to k-induction on control-flow paths [8]. Loop folding is a technique that aims to infer inductive invariants during BSE. Roughly speaking, when BSE starts from an error location and reaches a loop header, loop folding creates an initial invariant candidate that is disjoint with the current weakest precondition (i.e., the states that can reach the error location). If the invariant candidate is actually an invariant, we know that the error location is not reachable via the explored path. Otherwise, a pre-image of the invariant candidate along a loop path is computed, over-approximated, and added to the candidate. This process is repeated until an invariant is found or until it fails for some reason, e.g., when it discovers that the error location is actually reachable. Loop folding can infer complex disjunctive invariants and since it uses the error states, it is also property-driven.

String Analysis and Other Improvements The second major improvement in Symbiotic 9 is in the instrumentation for the property valid-memsafety. We have improved the analysis for the identification of out-of-bounds array accesses.

In Symbiotic 8, this analysis only determined whether an array access done via the index variable is in bounds [14]. The analysis in Symbiotic 9 also handles more general patterns where the array contains a concrete value (0 in the case of C strings) and the index pointer is incremented by one until it points to this concrete value, and where the pointer is incremented a fixed number of times.

Further, we have extended the forward symbolic execution in Slowbeast to handle parallel programs. For now, the symbolic execution is highly inefficient as it examines each interleaving of globally visible events. We plan to implement some reductions in the future. Slowbeast has been also extended to generate witnesses as this functionality was missing. Notably, it can generate non-trivial correctness witnesses using the invariants computed by BSELF. Previous versions of Symbiotic generate only trivial correctness witnesses.

Slicing has been also improved. It now applies a fast and coarse slicing before the main slicing. The coarse slicing detects all basic blocks from which no slicing criterion (i.e., an instruction whose reachability and arguments should be preserved) is syntactically reachable and replaces them by calls to abort.

#### 2 Strengths and Weaknesses

Forward symbolic execution is unable to fully analyze unbounded loops or infinite execution paths. Hence, unless program slicing removes the unbounded computation from the program, forward symbolic execution cannot verify it. However, backward symbolic execution and BSELF can fully analyze at least some unbounded programs [8]. Still, both these methods are computationally complex as the number of paths they must search may be enormous and their exploration may involve many non-trivial calls to the SMT solver. Therefore, these methods do not scale to real-world programs.

A strong aspect of Symbiotic is the very interplay of fast static analyses in the instrumentation, program slicing, and forward and backward symbolic execution. Fast static analyses are able to deem correct many parts of the code (with respect to the verified property). These parts of the code are then usually removed by slicing and only the possibly unsafe parts of the program (and their dependencies) get into a symbolic executor. In this sense, Symbiotic does incremental or conditional [3] verification.

Results of Symbiotic 9 in SV-COMP 2022 In SV-COMP 2022 [1], Symbiotic 9 won categories MemSafety, SoftwareSystems, and Overall, and got the 3rd place in FalsificationOverall. Moreover, it produced 1529 correct answers that were not confirmed, which is the highest number in SV-COMP 2022. 1073 unconfirmed answers are in MemSafety-Juliet, where we produced some incorrect witnesses due to a bug. Another 258 unconfirmed answers are in Termination. Symbiotic 9 produced only 3 incorrect answers caused by a bug in the replay mode of Slowbeast.

#### 3 Software Project and Contributors

All components of Symbiotic 9 use llvm 10 [10]. Slicer and instrumentation module are written in C++ and extensively use the library DG [5]. Klee is implemented in C++ and Slowbeast [12] is written in Python. Both symbolic executors use Z3 [11] as the SMT solver. Control scripts are written in Python.

Symbiotic 9 and all its components and external libraries are available under open-source licenses that comply with SV-COMP's policy for the reproduction of results. Symbiotic 9 participated in all categories of SV-COMP 2022 except the categories with Java programs.

Symbiotic 9 has been developed by Marek Chalupa, Vincent Mihalkoviˇc, Anna Recht´aˇckov´a, and Luk´aˇs Zaoral under the supervision of Jan Strejˇcek. ˇ

Data Availability Statement. All data of SV-COMP 2022 are archived as described in the competition report [1] and available on the competition web site. This includes the verification tasks, results, witnesses, scripts, and instructions for reproduction. The version of Symbiotic used in the competition is archived together with other participating tools [2] and also in its own artifact [6] at Zenodo.

# 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.

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. 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

# Symbiotic-Witch: A Klee-Based Violation Witness Checker? (Competition Contribution)

Paulína Ayaziová, Marek Chalupa , and Jan Strejček

Faculty of Informatics, Masaryk University, Brno, Czech Republic<EMAIL_ADDRESS>
Abstract. Symbiotic-Witch is a new tool for checking violation witnesses in the GraphML-based format used at SV-COMP since 2015. Roughly speaking, Symbiotic-Witch symbolically executes a given program with Klee and simultaneously tracks the set of nodes the witness automaton can be in. Moreover, it reads the return values of nondeterministic functions specified in the witness and uses them to prune the symbolic execution. The violation witness is confirmed if the symbolic execution reaches an error and the current set of witness nodes contains a matching violation node.

Symbiotic-Witch currently supports violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties.

# 1 Verification Approach

We present a new checker of violation witnesses called Symbiotic-Witch. The checker first loads a given violation witness in the GraphML format [5] and a given program. Then it performs symbolic execution [11] of the program and simultaneously tracks the progress of the execution in the witness automaton. More precisely, every state of symbolic execution is accompanied by the set of witness automaton nodes that can be reached under the executed program path. If the symbolic execution detects a violation of the considered property and the tracked set of witness automata nodes contains a violation node, the witness is confirmed.

Note that the original description of the witness format [5] does not provide any formal semantics of the format. We interpret it in the way that if an edge in a witness automaton matches an executed program instructions, then we can follow the edge but we can also stay in its starting node. Hence, if we have the set of witness automaton nodes reached under a certain program path, then prolongation of this path can add some nodes to this set, but it never removes any node from the set. A brief reading of an upcoming detailed description of the format [4] reveals that it can be the case that an edge matching an executed program instruction has to be taken. If this is indeed the case, we will adjust

? This work has been supported by the Czech Science Foundation grant GA19-24397S.

our tool, but the current implementation and the following texts consider the former semantic.

Before Symbiotic-Witch starts the symbolic execution, we remove from the witness automaton all nodes that are not on any path from the entry node to a violation node. In general, witness automata are related to program executions using node and edge attributes. Symbiotic-Witch currently supports only some attributes of witness edges to map a program execution to a given witness automaton. Namely, it uses the line number of executed instructions, the information whether true or false branch is taken, and the information about entering a function or returning from a function. Additionally, if the witness automaton contains a single path from the entry node to a violation node and there is some information about return values of the \_\_VERIFIER\_nondet\_\* functions on this path, then we use these values in the symbolic execution of the program. Return values not provided in the witness are treated as symbolic values.

A more precise description of the approach can be found in the bachelor's thesis of P. Ayaziová [1].

#### 2 Software Architecture

The approach has been implemented in a tool called Symbiotic-Witch, which is basically a modification of the symbolic executor Klee [8]. More precisely, it is derived from the clone of Klee used in Symbiotic, which employs the SMT solver Z3 [13] and supports symbolic pointers, memory blocks of symbolic sizes etc. For parsing of witnesses in the GraphML format, we use the library RapidXML.

As Klee executes programs in llvm [12], a given C program has to be translated to llvm first. We use Clang for this translation as explained in Section 4.

The current version of Symbiotic-Witch runs on llvm version 10.0.0.

#### 3 Strengths and Weaknesses

Existing violation witness checkers (excluding Dartagnan [10] designed for concurrent programs) can be roughly divided into two categories.

– CPA-witness2test [6], FShell-witness2test [6], and Nitwit [14] perform one program execution based on the information in the witness. If this execution violates the specification, the witness is confirmed. This approach is very efficient for witnesses fully describing one program execution that violates the property. However, if a witness describes more program executions and only some of them violate the property, these tools can easily miss the violating executions. In particular, if a witness does not specify some return value of a \_\_VERIFIER\_nondet\_\* function, FShell-witness2test uses the default value 0, Nitwit picks a random value, and CPA-witness2test fails the witness confirmation.

– CPAchecker [5], UltimateAutomizer [5], and MetaVal [7] create a product of a given witness automaton and the original program and analyze it. As a result, some execution paths of the original program can be analyzed repeatedly for different paths in the witness automaton. To suppress this effect, these checkers usually ignore the possibility to stay in a witness automaton node whenever there is a matching transition leaving the node. Unfortunately, a valid witness can be unconfirmed due to this strategy.

We believe that our approach to checking violation witnesses removes all mentioned disadvantages. Symbolic execution allows us to efficiently examine many program executions corresponding to a given witness automaton, and program executions are not analyzed repeatedly. The approach can easily handle witnesses based on return values from the \_\_VERIFIER\_nondet\_\* functions as well as those based on description of branching.

There is only one principal case when a valid witness is not confirmed by Symbiotic-Witch (ignoring the cases when Symbiotic-Witch simply runs out of resources). This case can arise when Symbiotic-Witch uses the information about return values of \_\_VERIFIER\_nondet\_\* functions stored in the witness. Symbiotic-Witch uses the information immediately when the symbolic execution calls such a function and there is a matching edge in the witness with a return value that has not been used yet (i.e., the starting node of the edge is in the set of tracked witness nodes and the target node is not). This "eager approach" usually works very well, especially for witnesses containing return values for all calls of \_\_VERIFIER\_nondet\_\* functions. However, there can be witnesses where some return values are missing and a particular contained return value should not be used for the first matching call of the \_\_VERIFIER\_nondet\_\* function. Such witnesses can be valid, but Symbiotic-Witch can fail to confirm them. As far as we know, such witnesses do not appear in SV-COMP and other witness checkers would probably fail to confirm them as well.

On the negative side, our approach inherits the disadvantages and limitations of symbolic execution and Klee. In particular, it can suffer the path explosion problem on witnesses that do not provide return values of \_\_VERIFIER\_nondet\_\* functions. Further, Symbiotic-Witch does not support parallel programs as Klee does not support them.

Our current approach is suitable for cases when a witness can be checked based on a finite program execution. That is why our tool supports violation witnesses of safety properties. Table 1 shows the numbers of violation witnesses confirmed in SV-COMP 2022 [2] by individual witness checkers in the categories supported by Symbiotic-Witch.

We believe that symbolic execution can be also used for checking termination violation witnesses and for checking correctness witnesses. We plan to extend Symbiotic-Witch in these directions. We also plan to add a witness refinement mode [5] already provided by CPAchecker and UltimateAutomizer. In this mode, when a witness is confirmed, Symbiotic-Witch would produce another witness describing a single program execution (by specifying return values for all calls of \_\_VERIFIER\_nondet\_\* functions) that exhibits the property violation.

Table 1. The numbers of confirmed witnesses in relevant SV-COMP 2022 categories

# 4 Tool Setup and Configuration

For the use in SV-COMP 2022, we have integrated our witness checker (originally called Witch-Klee) with Symbiotic [9], which takes care of translation of a given C program into llvm using Clang and then slightly modifies the llvm program to improve the efficiency of witness checking.

The archive with Symbiotic-Witch can be downloaded from SV-COMP archives. The witness checking process is invoked by

./symbiotic [–prp <prop>] [–32] –witness-check <wit.graphml> <prog.c>

where <wit.graphml> is a violation witness to be checked and <prog.c> is the corresponding program. By default, the tool considers reachability safety property and 64-bit architecture. The considered property can be changed by the –prp option and <prop> instantiated to memsafety or memcleanup or no-overflow. The 32-bit architecture is set by –32.

Our witness checker can be also downloaded directly from its repository mentioned below. The version used in SV-COMP 2022 is marked with the tag SV-COMP22. It can be executed without Symbiotic via a shell script as

./witch.sh <prog.c> <wit.graphml>

which calls Clang to translate <prog.c> to llvm and then passes the llvm program and the witness <wit.graphml> to the witness checker.

## 5 Software Project and Contributors

Symbiotic-Witch has been developed at Faculty of Informatics, Masaryk University by Paulína Ayaziová under the guidance of Marek Chalupa and Jan Strejček. The tool is available under the MIT license and all used tools and libraries (llvm, Klee, Z3, RapidXML, Symbiotic) are also available under open-source licenses that comply with SV-COMP's policy for the reproduction of results. The source code of our witness checker can be found at:

https://github.com/ayazip/witch-klee

Data Availability Statement. All data of SV-COMP 2022 are archived as described in the competition report [2] and available on the competition web site. This includes the verification tasks, results, witnesses, scripts, and instructions for reproduction. The version of Symbiotic-Witch used in the competition is archived together with other participating tools [3].

# References

14. Švejda, J., Berger, P., Katoen, J.: Interpretation-based violation witness validation for C: NITWIT. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12078, pp. 40–57. Springer (2020), https://doi.org/10.1007/978-3-030-45190-5\_3

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.

# Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)

Zs´ofa Ad´am ´ 1 , Levente Bajczi1 , Mih´aly Dobos-Kov´acs1 , Akos Hajdu ´ 2 , and Vince Moln´ar1 ⋆(B)

1 Department of Measurement and Information Systems Budapest University of Technology and Economics, Budapest, Hungary<EMAIL_ADDRESS>2 Meta Platforms Inc., London, United Kingdom

Abstract. Theta is a model checking framework based on abstraction refnement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for nonprogressing refnement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.

# 1 Verifcation Approach and Software Architecture

Theta [10] is a generic and confgurable model checking framework written in Java 11. A simplifed version of the architecture (focusing on software verifcation aspects) can be seen in Figure 1.

Fig. 1. Architecture of Theta.

The input is a C program that is frst translated to extended control-fow automata (XCFA). Previously, Theta used LLVM [3], which had various advantages, but its static single assignment (SSA) form proved overall disadvantageous for abstraction-based algorithms. This year we use a new, direct translation (no

⋆ Jury member representing Theta at SV-COMP 2022.

intermediate language and SSA form) via an ANTLR parser. Furthermore, the CFA being "extended" refers to the fact that since this year we support concurrent programs by an analysis with interleaving semantics. After parsing we apply various passes to the XCFA (e.g., large-block encoding or partial order reduction). The core of Theta is a CEGAR-based analysis framework, targeting reachability properties via predicate and explicit analyses [8], along with interpolation and Newton-based refnements [7]. This year, Theta added generic support for SMT solvers (including interpolation) via the SMT-LIB interface. At SV-COMP'22 we use CVC4 [4], MathSAT [6], and Z3 [9], where the latter is used via the Java API from before. Finally, a verdict (safe, unsafe, unknown) and a witness is produced corresponding to the C program (using metadata from the translation).

Fig. 2. Overview of the dynamic portfolio of Theta.

Verifcation portfolio. Based on preliminary experiments and domain knowledge, we manually constructed a dynamic algorithm selection portfolio [1] for SV-COMP'22, illustrated by Figure 2. Rounded white boxes correspond to decision points. We start by branching on the arithmetic (foats, bitvectors, integers). Under integers, there are further decision points based on the cyclomatic complexity and the number of havocs and variables. Grey boxes represent confgurations, defning the solver/domain/refnement in this order. Lighter and darker grey represents explicit and predicate domains respectively. Internal timeouts are written below the boxes. An unspecifed timeout means that the confguration can use all the remaining time. The solver can be CVC4 (C) [4], MathSAT (M), MathSAT with foats (Mf) [6] or Z3 (Z) [9]. Abstract domains are explicit values (E), explicit values with all variables tracked (EA), Cartesian predicate abstraction (PC) or Boolean predicate abstraction (PB) [8]. Finally, refnement can be Newton with weakest preconditions (N) [7], sequence interpolation (S) or backward binary interpolation (B) [8]. Arrows marked with a question mark (?) indicate an inconclusive result, that can happen due to timeouts or unknown results. Furthermore, this year's portfolio also includes a novel dynamic (run-time) check for refnement progress between iterations that can shut down potential infnite loops (by treating them as unknown result) [1]. Note also that for solver issues (e.g., exceptions from the solver) we have diferent paths in some cases.

## 2 Strengths and Weaknesses

Theta currently targets ReachSafety and ConcurrencySafety with limited support for structs, arrays and pointers, and no support for dynamic memory allocation, mutexes and recursion. Due to this, Theta fails for most tasks in ProductLines, Recursive, Heap and Arrays. Out of the 6163 tasks, roughly 2/3 can be translated and there are 888 confrmed correct (541 safe, 347 unsafe), 116 unconfrmed correct, and only 15 incorrect (11 false positive, 4 false negative) results [5]. Note that almost all unsupported cases are detected and reported as an error, and we only have a few incorrect results due to subtle issues.

The main strength of the tool is the combination of algorithm selection (pick algorithm based on input) and portfolios (try multiple algorithms until one succeeds). Out of the 1004 correct results, 315 could not be solved by the frst confguration that the portfolio tries: dynamic checks intervened for 181 internal timeouts, 72 solver issues (e.g. wrong models), 19 non-progressing refnements, and 74 other (unknown) faults before the eventual success.

Having a diverse portfolio also paid of. Bitvector and foat arithmetic tasks were either solved by explicit analyses (with a mixture of interpolation- and Newton-based refnements) before even trying predicate confgurations, or if explicit analyses failed, predicate confgurations were unsuccessful too. The integer arithmetic required a more diverse confguration set: Predicate abstraction solved roughly 48% of the tasks (45% Cartesian, 3% Boolean) and explicit analysis solved 52% (33% with empty precision, 19% with all variables tracked).

The SMT-LIB support provided a great improvement: previously we only had Z3, which still dominates the integer cases. However, all of the bitvector tasks were solved by MathSAT, making Z3 an unused backup. With foats, roughly half of the tasks were solved by MathSAT, while the other half needed CVC4 as backup. Since foats are reduced to bitvectors, we did not rely on Z3 based on poor performance in our preliminary experiments.

The most successful subcategories are BitVectors, ControlFlow, Loops, XCSP (38-45% correct), mostly because they use features of C that our frontend supports well. We plan to mitigate the high number of timeouts in the future with approximations (e.g. mixing integers and bitvectors), and further analyses (e.g., inferring loop invariants). We also have a signifcant amount of unconfrmed results: we believe this can be improved by generating more compact witnesses.

This year Theta added support for sequential concurrency via a preprocessing step: it yields an encoding where exploring all interleavings preserve interthread behaviors. The analyses treat consecutive non-global memory accesses as one atomic block, reducing the exploration of unnecessary total orders. A drawback of using preprocessing for partial order reduction instead of an on-line algorithm is the superfuous exploration of certain total orders, e.g., all interleavings of independent global memory accesses will also be explored. This is because such accesses might overlap with non-independent memory accesses at other times, and the preprocessing step is not aware of such details.

Using a wrapper, Theta integrates concurrency seamlessly with the existing framework (abstract domains, refnements), except the error location-based search [8] (used for non-concurrent cases) because the required distance metric is not well defned in concurrent programs. Instead, we opted to use a breadth-frst search, which had outperformed depth-frst strategies in preliminary tests. We theorize that this is due to bugs being reachable within the frst few instructions most of the time, but only via a specifc total order. The performance for concurrent programs is still limited though, and we plan to integrate a declarative approach in the future, which could be used for weakly-ordered programs as well.

# 3 Tool Setup and Confguration

The competition contribution is based on Theta 3.0.0-svcomp22-v1.3 Additionally, Theta uses CVC4 v1.9, MathSAT v5.6.6 and Z3 v4.5.0. The project's repository contains build instructions, but an archive can be found at the SV-COMP repository4 and Zenodo [2]. with pre-built binaries for Ubuntu 20.04 (LTS). The toolchain requires packages openjdk-11-jre-headless, libgomp1 and libmpfr-dev to be installed. The entry point of the toolchain is the script theta/theta-start.sh, which takes the verifcation task (C program) as its only mandatory input and runs the portfolio. As additional arguments we use --portfolio COMPLEX --witness-only --loglevel RESULT. Additional arguments are described in the readme included with the binaries.

# 4 Software Project

Theta is maintained by the Critical Systems Research Group5 of the Budapest University of Technology and Economics with various contributors. The project is available open-source on GitHub3 under an Apache 2.0 license.

Data Availability. The version of Theta used in this paper is available at [2].

Acknowledgment and Funding. The authors would like to thank Tam´as T´oth, Mil´an Mondok, Istv´an Majzik, Zolt´an Micskei and Andr´as V¨or¨os for their contributions to the project; and the competition organizers, especially Dirk Beyer for their help during the preparation for SV-COMP. The research contributions of the authors from the Budapest Univ. of Tech. and Econ. were funded by the EC and NKFIH through the Arrowhead Tools project (EU grant No. 826452, NKFIH grant 2019-2.1.3-NEMZ ECSEL-2019-00003), and by the UNKP-21-2 New National Excellence Program of ITM from the NRDI Fund.

3 https://github.com/ftsrg/theta/releases/tag/svcomp22-v1

4 https://gitlab.com/sosy-lab/sv-comp/archives-2022/-/blob/main/2022/theta.zip

5 https://ftsrg.mit.bme.hu

# 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.

# Ultimate GemCutter and the Axes of Generalization (Competition Contribution)

Dominik Klumpp?1 , Daniel Dietsch1 , Matthias Heizmann1 , Frank Sch¨ussele1 , Marcel Ebbinghaus1 , Azadeh Farzan2 , and Andreas Podelski1

> 1 University of Freiburg, Freiburg im Breisgau, Germany<EMAIL_ADDRESS>2 University of Toronto, Toronto, Canada

Abstract. Ultimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the Ultimate family.

# 1 Verification Approach

Ultimate GemCutter is a verification tool for concurrent programs based on the CEGAR paradigm: It (1) picks a trace from the set of all program interleavings (a possible "counterexample"), (2) proves correctness of this trace (the counterexample is "spurious"), and (3) generalizes the proof to conclude that a larger (usually infinite) set of traces is correct. Classically, CEGAR focuses on generalization across traces with varying numbers of loop iterations, by finding inductive loop invariants. GemCutter proposes additional generalization along

an orthogonal axis: across interleavings. Concurrent programs contain many redundant interleavings of actions from different threads, i.e., interleavings with the same (input/output-) behaviour. A na¨ıve application of CEGAR requires explicit proofs of correctness for all these interleavings. Intermediate states during execution of redundant interleavings differ, and different interleavings often require different correctness proofs. Gem-

Cutter addresses this as illustrated in the figure on the right: We prove correctness of a trace τ , here τ = a1a2b, where a1, a2 are actions of the first thread,

? Jury Member: Dominik Klumpp

and b is an action of the second thread. The proof of correctness is generated using Craig interpolation or similar techniques. We generalize this proof into a Floyd-Hoare automaton [8] to show that a regular language L (green area in the figure above) of traces is correct. The new contribution is the subsequent generalization step: If a trace τ1 differs from a (correct) trace τ2 in L only by the ordering of independent statements, these traces are (Mazurkiewicz-) equivalent [3]. We conclude that τ1 is also correct. Hence, the set of all such traces, denoted cl(L) (pink area), contains only correct traces. If the set of all program interleavings P is a subset of cl(L), we conclude that the program is correct.

To soundly make this conclusion, we need a suitable notion of independence between statements, which guarantees that the order of execution of two independent statements does not matter for program correctness. An intuitive sufficient condition is that neither statement writes to a memory location read or written by the other statement. If we cannot establish this condition syntactically, we use an SMT solver to check if executing the statements in either order is guaranteed to give the same result. We use information from the Floyd-Hoare automaton to refine this check in the style of conditional independence [5]. Such information can for instance express (but is not limited to) non-aliasing of pointers.

However, the inclusion P ⊆ cl(L) is in general undecidable [3]; cl(L) may not be regular. We reverse our viewpoint to provide a sufficient condition that can be effectively checked: Rather than adding all equivalent traces to L – thus obtaining cl(L) –, we instead remove all but one trace of each equivalence class from P – yielding a reduction P 0 of P (formally, cl(P 0 ) = P). We use the sleep set technique [5] to remove transitions from an automaton for P to get an automaton that recognizes one such reduction P 0 . We then check whether the (regular) reduction P 0 is included in the (regular) language L. If this inclusion P 0 ⊆ L holds, it implies that P ⊆ cl(L) also holds, and the program is correct. If the inclusion does not (yet) hold, GemCutter picks another program trace and repeats the process, iteratively building up the language L of correct traces by taking the union of the Floyd-Hoare automata computed in all iterations.

A key feature of the reduction-based approach is that the generalization along the iteration and interleaving axes is combined not just additively, but multiplicatively: In the geometrical intuition of the figure above, we do not just take the union of L (green area) with the equivalence class [τ ] of τ (blue area), but consider all traces in cl(L) (the pink area which is spanned by both). Further, we heuristically try to pick a set of representatives in a way that harmonizes

with CEGAR generalization, i.e., a reduction P 0 with simple loop invariants. To this end, we prefer representatives with context-switches at all loop boundaries. Ideally, each thread performs one complete loop iteration and then hands control over to the next thread (the last thread hands back control to the first thread). Consider the example program on the right, with the postcondition x = y. Here, a proof for the

```
// Thread 1:
int x = 0;
for (int i = 0; i < N; ++ i) {
  x += A[i ];
}
```

```
// Thread 2:
int y = 0;
for (int j = 0; j < N; ++ j) {
  y += A[j ];
}
```
set of all interleavings P, or some inopportunely chosen reduction, needs invariants that capture the fact that x = Pi k=0 A[k], and similar for y. Such invariants are usually not found by Craig interpolation. However, the loop invariant i = j ∧ x = y suffices for the reduction that places context-switches at all loop boundaries. The general idea is that for this kind of reduction, the proof often needs to summarize only the effect of a single loop iteration rather than unboundedly many iterations (which may require quantifiers or non-linear arithmetic). Similar observations were first made by Farzan and Vandikas [4].

GemCutter furthermore aims to improve efficiency of the proof check, i.e., the check whether a reduction P 0 is a subset of the set of proven traces L. The state explosion problem of concurrent programs makes the computation of an automaton recognizing a reduction P 0 as well as the subsequent inclusion check prohibitively expensive. To address this, we implemented a form of persistent set reduction [5], which allows us to compute a more compact automaton recognizing P 0 . This results in a more time- and memory-efficient inclusion check.

Reductions that interact harmoniously with CEGAR generalization do not always allow for an efficient proof check, nor vice versa. In the ConcurrencySafety category, where correctness proofs may become complicated, we prioritize generalization by computing reductions that typically allow for simpler proofs (described above), even though proof checking for such reductions is often more expensive. By contrast, in the NoDataRace category we found proof assertions to be usually quite simple (often only expressing non-aliasing of pointers), so we prioritize faster proof checks (and postpone context-switches as far as possible).

Implementation GemCutter uses the libraries and the front-end of the Ultimate framework, and extends Ultimate with a new CEGAR loop implementation and new algorithms operating on finite automata. We represent programs P, reductions P 0 and sets of proven traces L as finite automata. Ultimate constructs Floyd-Hoare automata (for L) only on-demand [7]. Due to the state explosion problem, GemCutter extends this approach to the program and the reduction. The necessary parts of the automata are constructed just-in-time during traversal by automata algorithms. Various techniques are implemented as instances of a few generic interfaces (on-demand automata, and visitors that monitor and guide automaton traversal) for flexibility: Radically different algorithms can be created by configuring, exchanging and stacking interface implementations. The following techniques and optimizations (all used in SV-COMP) can be combined with each other independently: (i) sleep set reduction; (ii) persistent set reduction; (iii) discovery and pruning of states that cannot reach accepting states; (iv) guidance towards representatives of a specific form, e.g. with context-switches at loop boundaries; and (v) inclusion check between automata.

#### 2 Strengths and Weaknesses

The main advantage over other concurrency approaches in Ultimate (in Automizer and Taipan) lies in the generalization across interleavings: Automizer and Taipan typically require more complex proofs possibly out-of-reach for Craig interpolation and similar techniques. GemCutter performs significantly better, winning 3rd place in the ConcurrencySafety category (behind the bounded model checkers Deagle [6] and CSeq [10]) and 1st place in the NoDataRace demo category. For details, refer to the competition report [1].

Since our proof check decides a stronger condition (P 0 ⊆ L), it might miss some cases in which the proof is actually sufficient, i.e., P ⊆ cl(L) holds. This is because P 0 and L might contain different representatives for the same equivalence class of interleavings. This weakness cannot be resolved completely due to the undecidability of the inclusion P ⊆ cl(L). It can however be attenuated by considering other choices of representatives (other than preferring contextswitches at loop boundaries) and exploring the effect. This choice is currently given as an input parameter; an approach that heuristically chooses a reduction based on the program structure might perform better. Our notion of independence between statements is currently ignorant of the specification being verified. We hope to extend our approach to take this into account. Finally, our approach (and implementation) can be easily extended with other reduction methods that correspond to more aggressive generalization along the interleaving axis.

Our approach only verifies programs with a bounded number of threads. GemCutter runs out of time or memory if it is unable to establish such an upper bound, e.g. for many benchmarks in pthread-ext/ or goblint-regression/.

# 3 Architecture, Setup, Configuration, and Project

GemCutter is part of the program analysis framework Ultimate3 , written in Java and licensed under LGPLv34 . GemCutter version 0.2.2-839c364b requires Java 11 and Python 3.6. Its Linux version, binaries of the required SMT solvers5 , and a Python wrapper script were submitted as a .zip archive. GemCutter is invoked with

./Ultimate.py --spec
 --file <f> --architecture  --full-output where
 is an SV-COMP property file, <f> is an input C file,  is the architecture (32bit or 64bit), and --full-output enables verbose output to stdout. A violation witness may be written to the file witness.graphml. The benchmarking tool BenchExec [2] supports GemCutter through the tool-info module ultimategemcutter.py6 . GemCutter participates in the ConcurrencySafety and NoDataRace categories, as declared in its SV-COMP benchmark definition file ugemcutter.xml7 .

Data Availability Our .zip archive is available online8 and on Zenodo [9].

3 ultimate.informatik.uni-freiburg.de and github.com/ultimate-pa/ultimate

4 www.gnu.org/licenses/lgpl-3.0.en.html

5 Z3 (github.com/Z3Prover/z3), CVC4 (cvc4.github.io) and Mathsat (mathsat.fbk.eu)

6 github.com/sosy-lab/benchexec/blob/main/benchexec/tools/ultimategemcutter.py

7 gitlab.com/sosy-lab/sv-comp/bench-defs/-/blob/main/benchmark-defs/ugemcutter.xml

8 gitlab.com/sosy-lab/sv-comp/archives-2022/-/blob/main/2022/ugemcutter.zip and git.io/JM69B

### 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.

# Wit4Java: A Violation-Witness Validator for Java Verifers (Competition Contribution)

Tong Wu1 , Peter Schrammel2 , and Lucas C. Cordeiro1 ()

1 University of Manchester, Manchester, United Kingdom 2 University of Sussex, Brighton, and Difblue Ltd, Oxford, United Kingdom<EMAIL_ADDRESS>
Abstract. We describe and evaluate a violation-witness validator for Java verifers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifer to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.

Keywords: Witness Validation · Software Verifcation · Java Bytecode.

# 1 Overview

Witness validation is the process of checking whether the same results can be reproduced independently according to the given program, specifcation, verifcation result, and the generated witness, improving the trust level of the software verifers [2].

Here, we describe and evaluate a new violation-witness validator for Java programs called Wit4Java. We take an approach similar to Rocha et al. [5] and Beyer et al. [1] for C programs and apply it to Java programs. As a result, we implement Wit4Java as a Python script that creates a new Java program or a unit test case using Mockito with the program variable values extracted from the counterexample. As input, Wit4Java uses the violation-witness in the GraphML format to extract the value of the non-deterministic variables in Java programs. Lastly, Wit4Java runs the new created program using the Java Virtual Machine (JVM) to check the assert statements.

There are some validators for C programs in the literature [6,12]. For example, NitWit is an interpretation-based witness validator that can execute each statement step-by-step without compiling the entire program [12]. The concept of MetaVal is to generate a new program based on the input and then use any checker to check for specifcations [6]. CPA-witness2test and FShell-witness2test are execution-based validators for C programs that can process the witness in

GraphML format and generate a test harness that drives the program to the specifcation violation [1]. Rocha et al. focus on the counterexample produced by ES-BMC [4] while CPA-witness2test and FShell-witness2test can process GraphML fles. However, witness validation for SV-COMP's Java track [7] is still at an early stage. GWIT is another validator that uses assumptions to prune the search space for dynamic symbolic execution, limiting the analysis to paths where a given assumption holds [10,11].

Fig. 1. Wit4Java Architecture. The grey boxes represent the inputs and outputs, and the white boxes represent the validation process.

#### 2 Validation Approach

The architecture of Wit4Java is illustrated in Fig. 1. First, Wit4Java takes the Java program and the witness as input. Then, it uses the Python package NetworkX to read the graph content of the witness and extracts the counterexample values of the variables corresponding to the source program from the violationwitness and saves them. After that, it generates new programs that contain the witness's assumptions. Finally, the validation process is performed by the JVM (using the -ea option) to check whether the execution of the generated program exhibits the detected assertion failure.

There are two implementations (Wit4Java 1.0 and Wit4Java 2.0) to extract and use counterexamples. The frst version is to save them as tuples (linenum, counterexample). Then it reads the source program and replaces the variables of the program statements with counterexamples if the line number and variable in the program match the tuple, thus generating a new created Java program. In comparison, the second version records the data types and values of the counterexamples and saves them sequentially into two lists. Moreover, only the assumptions made in the witness for the non-deterministic variables (as determined by Verifer.nondet) are recorded. Then, it builds a unit test case and employs the Mockito framework to mock the Verifer.nondet calls in the source program to make them return deterministic counterexample values from the lists. This makes the execution of the source program follow the path described in the witness and eventually reach the violated property.

We show examples for both implementations in Listings 1.1 to 1.4. Wit4Java 1.0 (the naive version) saves the counterexamples in witness in line number order. It directly replaces the variable values in the source program, thus generating a new program (cf. Listing 1.2). Wit4Java 2.0 (We name it the Mockito version) generates a test case that returns the counterexample value when the mocked function is called (cf. Listing 1.4).

```
Listing 1.3. Violation witness
< edge source ="203.167" target ="207.186" >
       < data key =" originfile ">
       Main . java
       </ data >
       < data key =" startline " >
       13
       </ data >
       < data key =" assumption ">
       v1 = 1;
       </ data >
</ edge >
 < edge source ="207.186" target ="252.201" >
       < data key =" originfile ">
       Main . java
       </ data >
       < data key =" startline " >
       14
       </ data >
       < data key =" assumption ">
       v2 = 0;
       </ data >
 </ edge >
                                                     Listing 1.4. Output of Wit4Java 2.0
                                                  List_type = [ int , int ];
                                                  List_value = [1 , 0];
                                                  Mockito . mockStatic ( Verifier . class );
                                                  int n = List_type . length ;
                                                  OngoingStubbing < Integer >
                                                     stubbing_int = Mockito .
                                                       when ( Verifier . nondetInt ());
                                                  for ( int i = 0; i < n; i ++) {
                                                   if (" int " . equals ( List_type [i ])) {
                                                      stubbing_int = stubbing_int .
                                                        thenReturn ( Integer .
                                                           parseInt ( List_value [i ]));
                                                   }
                                                  }
                                                  Main . main ( new String [0]);
```
#### 3 Discussion of Strengths and Weaknesses

Fig. 2 on the left compares the validation results of the two validation tools Wit4Java and GWIT. The former is based on version 1.0 (naive version). The latter is based on violation-witnesses produced by GDart. The results indicate that Wit4Java has successfully validated 140 out of 302 witnesses, while GWIT correctly validates 150 results. Version 2.0 handles counterexamples with diferent values for each iteration within a loop better than version 1.0. This is because version 1.0 skips the counterexamples before the last iteration. However, version 2.0 can fully use the counterexamples generated by each iteration. Fig. 2 on the right compares the validation results of the two versions of Wit4Java, which shows that version 2.0 (Mockito version) has a better validation ability (168 out of 302), thereby outperforming both version 1.0 and GWIT. However, the tool can only handle witnesses with concrete counterexamples. There are two main reasons why Wit4Java shows the result unknown: JBMC [3,8] produces an empty witness, or the witness does not contain a counterexample for a non-deterministic value. Besides, the validation for strings is not supported yet, which occurs in almost half of witnesses because JBMC does not yet output counterexample values for strings. Thus we were not able to test it. Generally, there are not enough

witnesses of high quality for testing the witness validator yet because JBMC sometimes correctly terminates without producing a witness in SV-COMP. The witness support in the Java verifers requires further development work so that they are able to produce complete violation witnesses whenever they terminate with verdict false.

Fig. 2. Validation results based on 302 witnesses. The x -axis represents the names of the two tools and the y-axis represents the number of witnesses. A green "false" indicates a confrmed correct result.

# 4 Tool Setup and Confguration

The competition submission is based on Wit4Java version 1.0 (naive version).3 For the competition [9], Wit4Java is called by executing the script wit4java.py. It reads .java source fles and corresponding witnesses in the given benchmark directories. The answer would be false if the assertion failure was found. As an example, we can validate the witness by executing the following command:

./wit4java.py -witness <path-to-sv-witnesses>/witness.graphml <path-to-svbenchmarks>/java/jbmc-regression/return2

where witness.graphml indicates the witness to be validated, and return2 indicates the benchmark name. The Benchexec tool info module is called wit4java.py and the benchmark defnition fle wit4java-validate-violation-witnesses.xml. NetworkX should be installed separately in the SV-COMP machines. If a validation task does not fnd a property violation, it will return unknown.

# 5 Software Project and Contributors

Tong Wu maintains Wit4Java. It is publicly available under a BSD-style license. The source code is available at https://github.com/Anthonysdu/wit4java, and instructions for running the tool are given in the README fle.

3 https://github.com/Anthonysdu/wit4java

# Acknowledgment

The work in this paper is partially funded by the EPSRC grants EP/T026995/1, EP/V000497/1, EU H2020 ELEGANT 957286, and Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme.

# 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.

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. 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

# **Author Index**

Ádám, Zsófia II-474 Aiken, Alex I-338 Aizawa, Akiko I-87 Albert, Elvira I-201 Alur, Rajeev II-353 Amat, Nicolas I-505 Amendola, Arturo I-125 Asgaonkar, Aditya I-167 Ayaziová, Paulína II-468 Bainczyk, Alexander II-314 Bajczi, Levente II-474 Banerjee, Tamajit II-81 Barbosa, Haniel I-415 Barrett, Clark I-143, I-415 Becchi, Anna I-125 Beyer, Dirk I-561, II-375, II-429 Biere, Armin I-443 Birkmann, Fabian II-159 Blatter, Lionel I-303 Blicha, Martin I-524 Bork, Alexander II-22 Bortolussi, Luca I-281 Bozzano, Marco I-543, II-273 Brain, Martin I-415 Bromberger, Martin I-480 Bruyère, Véronique I-244 Bryant, Randal E. I-443, I-462 Bu, Lei II-408

Casares, Antonio II-99 Cassez, Franck I-167 Castro, Pablo F. I-396 Cavada, Roberto I-125 Chakarov, Aleksandar I-404 Chalupa, Marek II-462, II-468 Cimatti, Alessandro I-125, I-543, II-273 Cohl, Howard S. I-87 Cordeiro, Lucas C. II-484 Coto, Alex II-413

D'Argenio, Pedro R. I-396 Darulova, Eva I-303 de Pol, Jaco van II-295

Deifel, Hans-Peter II-159 Demasi, Ramiro I-396 Dey, Rajen I-87 Dietsch, Daniel II-479 Dill, David I-183 Dobos-Kovács, Mihály II-474 Dragoste, Irina I-480 Duret-Lutz, Alexandre II-99 Dwyer, Matthew B. II-440

Ebbinghaus, Marcel II-479

Fan, Hongyu II-424 Faqeh, Rasha I-480 Farzan, Azadeh II-479 Fedchin, Aleksandr I-404 Fedyukovich, Grigory I-524, II-254 Ferrando, Andrea I-125 Fetzer, Christof I-480 Fijalkow, Nathanaël I-263 Fuller, Joanne I-167

Gallo, Giuseppe Maria I-281 Garhewal, Bharat I-223 Giannakopoulou, Dimitra I-387 Giesl, Jürgen II-403 Gipp, Bela I-87 González, Larry I-480 Goodloe, Alwyn I-387 Gordillo, Pablo I-201 Greiner-Petter, André I-87 Grieskamp, Wolfgang I-183 Griggio, Alberto II-273 Guan, Ji II-3 Guilloud, Simon II-196 Guo, Xiao II-408

Haas, Thomas II-418 Hajdu, Ákos II-474 Hartmanns, Arnd II-41 Havlena, Vojtˇech II-118 He, Fei II-424 Heizmann, Matthias II-479 Hensel, Jera II-403

Hernández-Cerezo, Alejandro I-201 Heule, Marijn J. H. I-443, I-462 Hovland, Paul D. I-106 Howar, Falk II-435, II-446 Hückelheim, Jan I-106 Huisman, Marieke II-332 Hujsa, Thomas I-505 Hyvärinen, Antti E. J. I-524 Imai, Keigo I-379 Inverso, Omar II-413 Jakobsen, Anna Blume II-295 Jonáš, Martin II-273 Kanav, Sudeep I-561 Karri, Ramesh I-3 Katoen, Joost-Pieter II-22 Katz, Guy I-143 Kettl, Matthias II-451 Klumpp, Dominik II-479 Koenig, Jason R.  I-46 Neider, Daniel I-263 Nenzi, Laura I-281 Neykova, Rumyana I-379 Niemetz, Aina I-415 Norman, Gethin II-60 Nötzli, Andres I-415

Ozdemir, Alex I-415

Padon, Oded I-338 Park, Junkil I-183 Parker, David II-60 Patel, Nisarg I-46 Paulsen, Brandon I-357 Pérez, Guillermo A. I-244 Perez, Ivan I-387 Pilati, Lorenzo I-125 Pilato, Christian I-3 Podelski, Andreas II-479 Ponce-de-León, Hernán II-418 Preiner, Mathias I-415 Pressburger, Tom I-387 Putruele, Luciano I-396

Qadeer, Shaz I-183 Quatmann, Tim II-22

Raha, Ritam I-263 Rakamari´c, Zvonimir I-404 Raszyk, Martin II-236 Rechtáˇ ˇ cková, Anna II-462 Reeves, Joseph E. I-462 Renkin, Florian II-99

Reynolds, Andrew I-415 Roˇckai, Petr II-457 Rot, Jurriaan I-223 Roy, Rajarshi I-263 Roy, Subhajit I-3 Rubio, Albert I-201 Rungta, Neha I-404 Safari, Mohsen II-332 Sakar, Ömer ¸ II-332 Sales, Emerson II-413 Santos, Gabriel II-60 Scaglione, Giuseppe I-125 Schmuck, Anne-Kathrin II-81 Schneider, Joshua II-236 Schrammel, Peter II-484 Schubotz, Moritz I-87 Schüssele, Frank II-479 Sharygina, Natasha I-524 Sheng, Ying I-415 Shenwald, Noam I-25 Shi, Lei II-353 Shoham, Sharon I-338 Sickert, Salomon II-99 Siegel, Stephen F. I-106 Šmahlíková, Barbora II-118 Sølvsten, Steffan Christ II-295 Soudjani, Sadegh II-81 Spiessl, Martin II-429 Staquet, Gaëtan I-244 Steffen, Bernhard II-314 Strejˇcek, Jan II-462, II-468 Sun, Dawei I-322 Sun, Zhihang II-424

Tabajara, Lucas M. I-64 Tacchella, Alberto I-125 Takhar, Gourav I-3 Thomasen, Mathias Weller Berg II-295 Tinelli, Cesare I-415

Tonetta, Stefano I-543 Traytel, Dmitriy II-236 Trost, Avi I-87 Tuosto, Emilio II-413 Tzevelekos, Nikos II-178 Ulbrich, Mattias I-303 Vaandrager, Frits I-223 Vardi, Moshe Y. I-64 Vozarova, Viktoria I-543 Wang, Chao I-357 Wang, Hao II-217 Wang, Yuepeng II-353 Weidenbach, Christoph I-480 Wesselink, Wieger II-137 Wijs, Anton II-332 Willemse, Tim A. C. II-137 Wißmann, Thorsten I-223 Wu, Haoze I-143 Wu, Tong II-484 Wu, Wenhao I-106 Xie, Tao II-217 Xie, Zhunyi II-408 Xu, Meng I-183 Yi, Pu II-217 Youssef, Abdou I-87 Yu, Nengkun II-3 Zamboni, Marco I-125

Zaoral, Lukáš II-462 Zelji´c, Aleksandar I-143 Zhao, Jianhua II-408 Zhong, Emma I-183 Zilio, Silvano Dal I-505 Zingg, Sheila II-236 Zlatkin, Ilia II-254 Zohar, Yoni I-415