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

Last commit date

9 February 2018

Related papers

https://doi.org/10.1007/978-3-662-49674-9_69 (TACAS '16)

Last publication date

9 April 2016

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.