Electronic Proceedings in Theoretical Computer Science (Aug 2019)

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

  • Burak Ekici,
  • Arjun Viswanathan,
  • Yoni Zohar,
  • Clark Barrett,
  • Cesare Tinelli

DOI
https://doi.org/10.4204/EPTCS.301.4
Journal volume & issue
Vol. 301, no. Proc. PxTP 2019
pp. 18 – 26

Abstract

Read online

This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While many of these were proved in a completely automatic fashion for any bit-width, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over arbitrary bit-widths. In this paper we describe our initial efforts in proving a subset of these invertibility conditions in the Coq proof assistant. We describe the Coq library that we use, as well as the extensions that we introduced to it.