Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici (University of Innsbruck), Arjun Viswanathan (University, of Iowa), Yoni Zohar (Stanford University), Clark Barrett (Stanford, University), Cesare Tinelli (University of Iowa)
TL;DR
This paper discusses the formal verification of invertibility conditions for fixed-width bit-vectors in the Coq proof assistant, aiming to ensure correctness in SMT solving over arbitrary bit-widths.
Contribution
It introduces a Coq library and extensions for verifying invertibility conditions, advancing the formal proof efforts for bit-vector theories.
Findings
Successfully formalized a subset of invertibility conditions in Coq.
Extended the Coq library to support these formal proofs.
Lays groundwork for verifying more conditions in the future.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.