Book chapter
Formal Verification of Bit-Vector Invertibility Conditions in Coq
Frontiers of Combining Systems, pp.41-59
Lecture Notes in Computer Science, v. 14279, Springer Nature Switzerland
01/01/2023
DOI: 10.1007/978-3-031-43369-6_3
Abstract
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.
Details
- Title: Subtitle
- Formal Verification of Bit-Vector Invertibility Conditions in Coq
- Creators
- Burak Ekici - Muğla UniversityArjun Viswanathan - University of IowaYoni Zohar - Bar-Ilan UniversityCesare Tinelli - University of IowaClark Barrett - Stanford University
- Resource Type
- Book chapter
- Publication Details
- Frontiers of Combining Systems, pp.41-59
- Series
- Lecture Notes in Computer Science; v. 14279
- DOI
- 10.1007/978-3-031-43369-6_3
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer Nature Switzerland
- Language
- English
- Date published
- 01/01/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984501625202771
Metrics
62 Record Views