PV3 VVT: Vienna Verification Toolencodes an LLVM program into a transition relation and checks properties on it

Application domain/field

Expected input

Program

Format:

C/C++ and SMTLib2

Internals

VVT primarily targets the verification of infinite parallel programs. VVT consists of several tools Uses Z3 and MathSAT.
C C++

Links

Related papers

Vienna Verification Tool: IC3 for Parallel Software (TACAS '16)

Last publication date

9 April 2016

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.