FrankenBit

Gurfinkel, A., Belov, A.: FrankenBit: bit-precise verification with many bits. 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.

References in zbMATH (referenced in 3 articles )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  2. Demyanova, Yulia; Pani, Thomas; Veith, Helmut; Zuleger, Florian: Empirical software metrics for benchmarking of verification tools (2017)
  3. Gurfinkel, Arie; Belov, Anton: Frankenbit: Bit-precise verification with many bits. (Competition contribution) (2014) ioport