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 M. Chechik & J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 954–957). Springer. 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-04 - Forschungsbereich Formal Methods in Systems Engineering

Published in:

Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings

ISBN:

978-3-662-49673-2

Volume:

9636

DOI of the book:

10.1007/978-3-662-49674-9

Date (published):

2016

Event name:

TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016

Event date:

2-Apr-2016 - 8-Apr-2016

Event place:

Eindhoven, Netherlands (the)

Number of Pages:

Publisher:

Springer, Berlin, Heidelberg

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