FrankenBit
FrankenBit
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.
Bit-precise
A bit-precise verifier with bit-precise counterexamples and bit-precise inductive invariants.
LLVM/UFO Frontend
Based on LLVM/UFO front-end for parsing, inlining, and simplifying C code for analysis.
Awards
Silver (ControlFlow) and Bronze (DeviceDrivers64) medals at TACAS 2014 Competition on Software Verification (SV-COMP 2014).
Safe Inductive Invariant Synthesis
Discovers bit-precise inductive invariants by unsound (but efficient) approximations and sound invariant strenthening.
Bounded Model Checking
Leverages LLBMC to efficiently find bit-precise counterexamples.
Many bits
FrankenBit builds on many excellent tools, including Z3, LLVM, UFO, LLBMC, Misper, MUSer2, Boolector, MiniSAT, STP, AIGER, and Python to hold everyting in place