FrankenBit is a bit-precise software verifier that combines the power of bit-vector decision procedures with the power of invariant generalization of Linear Arithmetic.
A bit-precise verifier with bit-precise counterexamples and bit-precise inductive invariants.
Based on LLVM/UFO front-end for parsing, inlining, and simplifying C code for analysis.
Silver (ControlFlow) and Bronze (DeviceDrivers64) medals at TACAS 2014 Competition on Software Verification (SV-COMP 2014).
Discovers bit-precise inductive invariants by unsound (but efficient) approximations and sound invariant strenthening.
Leverages LLBMC to efficiently find bit-precise counterexamples.