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.
Cite
CITATION STYLE
Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna verification tool: IC3 for parallel software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 954–957). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_69
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
