Zur Seitenansicht
 

Titelaufnahme

Titel
Vienna Verification Tool: IC3 for Parallel Software
VerfasserGünther, Henning ; Laarman, Alfons ; Weissenbacher, Georg
Erschienen in
Tools and Algorithms for the Construction and Analysis of Systems / Chechik, Marsha; Raskin, Jean-François, Eindhoven, The Netherlands, 2016, S. 954-957
Erschienen2016
Ausgabe
Accepted version
SpracheEnglisch
SerieLecture Notes in Computer Science ; 9636
DokumenttypAufsatz in einem Sammelwerk
Schlagwörter (EN)model checking / multi-threading / concurrent software
Projekt-/ReportnummerFWF S11403-N23, WWTF VRG11-005
URNurn:nbn:at:at-ubtuw:3-2923 Persistent Identifier (URN)
DOI10.1007/978-3-662-49674-9_69 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Vienna Verification Tool: IC3 for Parallel Software [0.16 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

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 Liptons reduction to reduce the number of interleavings. This paper introduces VVT, its underlying architecture and use.