“Verifying
Bit-vector Invertibility Conditions in Coq (Extended Abstract)”
by Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, and Cesare Tinelli.
In *Proceedings of the Sixth Workshop on Proof eXchange for Theorem
Proving (PxTP '19)*, (Giselle Reis and Haniel Barbosa, eds.), Aug.
2019, pp. 18-26. Natal, Brazil.

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.

**BibTeX entry:**

@inproceedings{EVZ+19, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark Barrett and Cesare Tinelli}, editor = {Giselle Reis and Haniel Barbosa}, title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)}, booktitle = {Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP '19)}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {301}, pages = {18--26}, month = aug, year = {2019}, note = {Natal, Brazil}, url = {http://theory.stanford.edu/~barrett/pubs/EVZ+19.pdf} }

(This webpage was created with bibtex2web.)