Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Verification Approach

VVT is an implementation of the CTIGAR approach [2], an SMT-based IC3 algorithm [3] incorporating Counterexample-Guided Abstraction Refinement (CEGAR)  [5], thus enabling the verification of infinite-state systems. The underlying abstraction-refinement scheme follows the IC3 paradigm; it does not require an unwinding of the transition relation. To handle parallel programs, VVT uses a large-block encoding [8] that preserves all relevant partial interleavings by applying a novel dynamic variant of Lipton’s reduction [12].

2 Software Architecture

VVT uses a modular approach to verification: a collection of separate tools instrument and translate the input, communicating via standard data formats such as LLVM bitcode [4] and the SMTlib format [1]. Figure 1 provides an overview.

The verification process begins by compiling the C file into LLVM bitcode using CLang. The LLVM IR has a precise semantics and comprises only a small number of instructions, thus reducing the complexity of the verifier. The increase in size resulting from the translation into bitcode is mitigated by subsequent reduction steps. A separate tool implementing a variant of Lipton’s reduction [12] identifies large blocks that can be executed atomically. These blocks are delimited by instrumenting the code with ‘yield’ function calls, indicating the relevant context switches. Our novel dynamic reduction method avoids static analysisFootnote 1 by expressing reduction conditions as branches. At each intermediate step the LLVM tool chain is used to optimize the bitcode (not shown in the figure).

Fig. 1.
figure 1

Architecture

Full size image

Next, the vvt-enc tool translates the instrumented bitcode into an SMTlib-based format, encoding the transition relation of the program. It uses (linear) integer arithmetic to encode bit vectors to facilitate interpolation and employs alias-analysis techniques in order to keep the transition relation as small as possible. To finalize the encoding, the vvt-opt tool deploys a number of optimization techniques including program slicing (removing irrelevant parts of the transition relation), expression simplification and a value-set analysis (to identify constant expressions).

The last step is the actual verification with the vvt-verify tool. It uses Z3 [6] for IC3 consecution calls [3] and MathSAT [7] for interpolation-based refinement. To rapidly find counterexamples, VVT runs a small portfolio with the BMC tool vvt-bmc [11] on the same encoding (not shown in the figure), taking advantage of the modularity of the tool chain.

3 Strengths and Weaknesses

VVT primarily targets the verification of infinite parallel programs. Unlike BMC tools, the approach is complete and does not depend on a complete unrolling of the transition relation thanks to the underlying IC3 algorithm. The SMT-based abstraction-refinement scheme further extends the capabilities of the tool to infinite-state systems. Finally, parallelism is supported by the reductions applied to the transition relation.

Our experiments show that VVT yields good results on almost all instances of the concurrency category of the Software Verification Competition (SVCOMP) 2016. The verification results for integer/control-flow programs demonstrate that the abstraction-refinement mechanisms work well in practice.

VVT currently does not implement rely-guarantee reasoning, and is therefore unable to handle an infinite number of threads. Furthermore, the lack of an interpolating decision procedure for arrays limits the applicability of the tool for programs with arrays to those cases where the size of the arrays can be determined statically.

VVT generates concrete counterexample traces, but does not yet map the LLVM instructions to locations in the original source code.

4 Tool Setup and Configuration

The Vienna Verification Tool is open source and distributed under the GPL license. Both the source code and the packaged version 0.1 submitted to SVCOMP 2016 can be found at the VVT website [10].

Installation. VVT v0.1 [10] requires packages LLVM 3.5 and CLang 3.5, which are available via standard package managers (APT, RPM, etc.) on many systems.

The command vvt-svcomp-bench.sh <FILE> starts the entire verifier tool chain (see Fig. 1), where <FILE> is the C or C++ file to be verified.

Participation Statement. For the SVCOMP 2016, we enlist VVT for participation in the categories Integers and Control Flow and Concurrency. In the former, we opt out of the sub-categories: recursive, loops, product lines, and sequentialized. We also opt out VVT of the other (unmentioned) categories.

5 Software Project and Contributors

VVT is developed by the Formal Methods in Systems Engineering (FORSYTE) group of the Vienna University of Technology. For more information, contact Henning Günther. Bug reports and feature requests can be submitted via the VVT website [10].