Property Invariant Embedding for Automated Reasoning

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

6th Workshop on Proof eXchange for Theorem Proving, EPTCS 301, pp. 18 – 26, 2019.


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.


  PDF |    doi:10.4204/EPTCS.301.4  |  © Open Access (CC BY 4.0)


author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark W. Barrett and Cesare Tinelli},
title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)},
booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019},
pages = {18--26},
year = {2019},
url = {},
doi = {10.4204/EPTCS.301.4},
editor = {Giselle Reis and Haniel Barbosa},
series = {{EPTCS}},
volume = {301},
Nach oben scrollen