Verifying Bit-vector Invertibility Conditions in Coq (Extended 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 aut...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1908.09478v1 |
| _version_ | 1818018007246438400 |
|---|---|
| author | Burak Ekici Arjun Viswanathan Yoni Zohar Clark Barrett Cesare Tinelli |
| author_facet | Burak Ekici Arjun Viswanathan Yoni Zohar Clark Barrett Cesare Tinelli |
| author_sort | Burak Ekici |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-14T07:33:31Z |
| format | Article |
| id | doaj.art-05aa5ad7ef454eb39cdbfc45c402d87f |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-14T07:33:31Z |
| publishDate | 2019-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-05aa5ad7ef454eb39cdbfc45c402d87f2022-12-22T02:05:45ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-08-01301Proc. PxTP 2019182610.4204/EPTCS.301.4:5Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)Burak Ekici0Arjun Viswanathan1Yoni Zohar2Clark Barrett3Cesare Tinelli4 University of Innsbruck University of Iowa Stanford University Stanford University University of Iowa 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.http://arxiv.org/pdf/1908.09478v1 |
| spellingShingle | Burak Ekici Arjun Viswanathan Yoni Zohar Clark Barrett Cesare Tinelli Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) Electronic Proceedings in Theoretical Computer Science |
| title | Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) |
| title_full | Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) |
| title_fullStr | Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) |
| title_full_unstemmed | Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) |
| title_short | Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) |
| title_sort | verifying bit vector invertibility conditions in coq extended abstract |
| url | http://arxiv.org/pdf/1908.09478v1 |
| work_keys_str_mv | AT burakekici verifyingbitvectorinvertibilityconditionsincoqextendedabstract AT arjunviswanathan verifyingbitvectorinvertibilityconditionsincoqextendedabstract AT yonizohar verifyingbitvectorinvertibilityconditionsincoqextendedabstract AT clarkbarrett verifyingbitvectorinvertibilityconditionsincoqextendedabstract AT cesaretinelli verifyingbitvectorinvertibilityconditionsincoqextendedabstract |