“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.)