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

Application domain/field

• Infinite-state systems
• Counterexample-guided abstraction refinement (CEGAR)
• Predicate abstraction
• Model checking
• Bounded model checking

Expected input

Program

Format:

C/C++ and SMTLib2

Internals

VVT primarily targets the verification of infinite parallel programs. VVT consists of several tools

• vvt-enc to translate instrumented bitcode into an SMTLIB-based format
• vvt-opt to deploy several optimization techniques
• vvt-verify to verify the program
• vvt-bmc to rapidly find counterexamples

Uses Z3 and MathSAT.