Synthesizing safe bit-precise invariants

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. Although the problem is decidable and is reducible to propositional safety by bit-blasting, the approach does not scale in practice. The alternative approach of lifting propositional algorithms to bit-vectors is difficult. In this paper, we propose a novel technique that uses unsound approximations (i.e., neither over- nor under-) for synthesizing sound bit-precise invariants. We prototyped the technique using Z3/PDR engine and applied it to bit-precise verification of benchmarks from SVCOMP'13. Even with our preliminary implementation we were able to demonstrate significant (orders of magnitude) performance improvements with respect to bit-precise verificaton using Z3/PDR directy. © 2014 Springer-Verlag.