Vienna Verification Tool: IC3 for Parallel Software
- 1.3k Downloads
Recently proposed extensions of the IC3 model checking algorithm offer a powerful new way to symbolically verify software. The Vienna Verification Tool (VVT) implements these techniques with the aim to tackle the problem of parallel software verification. Its SMT-based abstraction mechanisms allow VVT to deal with infinite state systems. In addition, VVT utilizes a coarse-grained large-block encoding and a variant of Lipton’s reduction to reduce the number of interleavings. This paper introduces VVT, its underlying architecture and use.
KeywordsModel Check Transition Relation Software Verification Tool Chain Model Check Algorithm
1 Verification Approach
VVT is an implementation of the CTIGAR approach , an SMT-based IC3 algorithm  incorporating Counterexample-Guided Abstraction Refinement (CEGAR) , 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  that preserves all relevant partial interleavings by applying a novel dynamic variant of Lipton’s reduction .
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  and the SMTlib format . Figure 1 provides an overview.
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  for IC3 consecution calls  and MathSAT  for interpolation-based refinement. To rapidly find counterexamples, VVT runs a small portfolio with the BMC tool vvt-bmc  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 .
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
- 1.Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds,) SMT Workshopp (2010)Google Scholar
- 2.Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 829–846. Springer, Heidelberg (2014)Google Scholar
- 4.Lattner, C., Adve, V.: The LLVM Instruction Set and Compilation Strategy. Technical report UIUCDCS-R-2002-2292, University of Illinois (August 2002)Google Scholar
- 8.Beyer, D., et al. Software model checking via large-block encoding. In: FMCAD, pp. 25–32. IEEE (2009)Google Scholar
- 10.Günther, H.: VVT website. http://vvt.forsyte.at, last visited: January 2016
- 11.Günther, H., Weissenbacher, G.: Incremental bounded software model checking. In: SPIN, pp. 40–47. ACM (2014)Google Scholar