A Framework for LLVM Code Verification

The Vienna Verification Toolkit (VVT for short) is a collection of programs and libraries for program verification. The programs of the toolkit include:

A tool to encode an LLVM program into a transition relation which can then be processed by the rest of the tools called vvt-enc
By using different techniques such as program slicing, constant propagation and expression simplification vvt-opt can be used to optimize a transition relation.
vvt-verify is used to verify that a given transition relation contains no bugs using a combination of IC3 and predicate abstraction.
To quickly find bugs in a transition relation, vvt-bmc employs bounded model checking to uncover them.