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