Abstract
Bit-precise software verification is an important and difficult problem. While there has been an amazing progress in SAT solving, Satisfiability Modulo Theory of Bit Vectors, and bit-precise Bounded Model Checking, proving bit-precise safety, i.e. synthesizing a safe inductive invariant, remains a challenge. In this paper, we present FrankenBit - a tool that combines bit-precise invariant synthesis with BMC counterexample search. As the name suggests, FrankenBit combines a large variety of existing verification tools and techniques, including LLBMC, UFO, Z3, Boolector, MiniSAT and STP. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Gurfinkel, A., & Belov, A. (2014). FrankenBit: Bit-precise verification with many bits (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 408–411). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_32
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
