A Framework for LLVM Code VerificationThe 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.