Vienna Verification Tool: IC3 for Parallel Software

Günther, Henning; Laarman, Alfons; Weissenbacher, Georg

doi:10.1007/978-3-662-49674-9_69

Record link:

https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-2923
http://hdl.handle.net/20.500.12708/344

Title:

Vienna Verification Tool: IC3 for Parallel Software

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, The Netherlands. https://doi.org/10.1007/978-3-662-49674-9_69

CatalogPlus:

AC11361644

Publisher DOI:

10.1007/978-3-662-49674-9_69

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Günther, Henning
Laarman, Alfons
Weissenbacher, Georg

Organisational Unit:

E192 - Institut für Informationssysteme

Volume:

9636

Date (published):

2016

Publisher:

Eindhoven, The Netherlands

Keywords:

model checking; multi-threading; concurrent software

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.

Additional information:

The final publication is available via <a href="https://doi.org/10.1007/978-3-662-49674-9_69" target="_blank">https://doi.org/10.1007/978-3-662-49674-9_69</a>.

License:

In Copyright

Appears in Collections:

Conference Paper