Title: Vienna Verification Tool: IC3 for Parallel Software
Language: English
Authors: Günther, Henning 
Laarman, Alfons 
Weissenbacher, Georg
Issue Date: 2016
Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna Verification Tool: IC3 for Parallel Software. In Tools and Algorithms for the Construction and Analysis of Systems ; Chechik, Marsha; Raskin, Jean-François. Eindhoven. https://doi.org/10.1007/978-3-662-49674-9_69
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.
Keywords: model checking; multi-threading; concurrent software
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-2923
Library ID: AC11361644
Organisation: E192 - Institut für Informationssysteme 
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

Page view(s)

checked on Sep 15, 2021


checked on Sep 15, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.