Title: Vienna Verification Tool: IC3 for Parallel Software
Language: English
Authors: Günther, Henning 
Laarman, Alfons 
Weissenbacher, Georg
Issue Date: 2016
Citation: 
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
Abstract: 
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
http://hdl.handle.net/20.500.12708/344
Library ID: AC11361644
Organisation: E192 - Institut für Informationssysteme 
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:


Page view(s)

112
checked on Sep 15, 2021

Download(s)

227
checked on Sep 15, 2021

Google ScholarTM

Check


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