Verified Isabelle/HOL tactic for the theory of bounded integers based on quantifier instantiation and SMT

SMT solvers are widely applied for deductive verification of C programs using various verification platforms (Why3, Frama-C/WP, F*) and interactive theorem proving systems (Isabelle, HOL4, Coq) as the decision procedures implemented in SMT solvers are complete for some combinations of logical theories (logics), in particular for the QF_UFLIA logic. At the same time, when verifying C programs, it is often necessary to discharge formulas in other logical theories and their combinations, that are also decidable but not supported by all SMT solvers. Theories of bounded integers both with overflow (for unsigned integers in C) and without overflow (for signed integers), and also theory of finite interpreted sets (needed to support frame conditions) are good examples of such theories. One of the possible ways to support such theories is to directly implement them in SMT-solvers, however, this method is often time-consuming, as well as insufficiently flexible and universal. Another way is to implement custom quantifier instantiation strategies to reduce formulas in unsupported theories to formulas in widespread decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded integers without overflow into the  QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle. The paper presents an informal description of this proof as well as some considerations on the efficiency of the proposed procedure. Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

1. T. Nipkow, M. Wenzel, and L.C. Paulson (editors). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science book series, vol. 2283, 2002, 218 p.

2. J. Dawson. Isabelle theories for machine words. Electronic Notes in Theoretical Computer Science, vol. 250, no. 1, 2009, pp. 55-70.

3. D. Babic and M. Musuvathi. Modular arithmetic decision procedure. Technical Report MSR-TR-2005-114, Microsoft Research, 2005.

4. N. Bjørner, A. Blass, Y. Gurevich, and M. Musuvathi. Modular difference logic is hard. Technical Report MSR-TR-2008-140, Microsoft Research, 2008.

5. B.-Y. Wang. On the satisfiability of modular arithmetic formulae. Lecture Notes in Computer Science book series, vol. 4218, 2006, pp. 186–199.

6. S. Böhme. Proof reconstruction for Z3 in Isabelle/HOL. In Proc. of the 7th International Workshop on Satisfiability Modulo Theories (SMT ’09), 2009.

7. S. Böhme and T. Weber. Fast LCF-style proof reconstruction for Z3. Lecture Notes in Computer Science book series, vol. 6172, 2010, pp. 179–194.

8. C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. Department of Computer Science, The University of Iowa, Technical Report, 2017.

9. R. Sadykov and M. Mandrykin. Completeness of instantiation procedure for bounded linear integer arithmetic. Formalization in Isabelle/HOL. Anailable at: https://forge.ispras.ru/projects/tsmt/repository/, accessed April 2020.

10. D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. Lecture Notes in Computer Science book series, vol. 7406, 2012, pp. 99–115.

11. Kovásznai G. How Har is Bit-Precise Reasoning? In Proc. of the 10th International Conference on Applied Informatics, 2017. pp. 179-190.