“Formal
Verification of Bit-Vector Invertibility Conditions in Coq”
by Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, and Clark Barrett.
In *Proceedings of the 14^th International Symposium on
Frontiers of Combining Systems (FroCoS '23)*, (Uri Sattler and Martin
Suda, eds.), Sep. 2023, pp. 41-59. Prague, Czech Republic.

We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors — used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5 — in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. In this paper we describe the process of proving a representative subset of these invertibility conditions in Coq. In particular, we describe the BVList library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions.

**BibTeX entry:**

@inproceedings{EVZ+23, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Cesare Tinelli and Clark Barrett}, editor = {Uri Sattler and Martin Suda}, title = {Formal Verification of Bit-Vector Invertibility Conditions in Coq}, booktitle = {Proceedings of the {\it 14^{th}} International Symposium on Frontiers of Combining Systems (FroCoS '23)}, series = {Lecture Notes in Artificial Intelligence}, volume = {14279}, pages = {41--59}, publisher = {Springer}, month = sep, year = {2023}, doi = {10.1007/978-3-031-43369-6_3}, note = {Prague, Czech Republic}, url = {https://link.springer.com/chapter/10.1007/978-3-031-43369-6_3} }

(This webpage was created with bibtex2web.)