Effective Word-Level Interpolation for Software Verification

We present an interpolation procedure for the theory of fixed-size bit-vectors, which allows to apply effective interpolation-based techniques for software verification without giving up the ability of handling precisely the word-level operations of typical programming languages.

Our algorithm is based on advanced techniques for Satisfiability Modulo Theories, and, although general, is optimized to exploit the structure of typical interpolation problems arising in software verification. 

We discuss the main ideas of the algorithm and present its implementation within the MathSAT SMT solver and the Kratos software model checker, showing very promising empirical results on programs requiring bit-precise modelling of word-level operations.