Vienna Verification Tool: IC3 for Parallel Software

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

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

Datensatz Zitierlink:

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

Titel:

Vienna Verification Tool: IC3 for Parallel Software

Zitat:

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

Verlags-DOI:

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

Publikationstyp:

Konferenzbeitrag - Full-Paper Contribution

Sprache:

Englisch

Autor_innen:

Günther, Henning
Laarman, Alfons
Weissenbacher, Georg

Organisationseinheit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Erschienen 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

Band:

9636

DOI des Buches:

10.1007/978-3-662-49674-9

Datum (veröffentlicht):

2016

Veranstaltungsname:

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

Veranstaltungszeitraum:

2-Apr-2016 - 8-Apr-2016

Veranstaltungsort:

Eindhoven, Niederlande (die)

Umfang:

Verlag:

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.

Weitere 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>.

Lizenz:

Urheberrechtsschutz

Enthalten in den Sammlungen:

Conference Paper