| dc.contributor.author | Ekici, Burak | |
| dc.contributor.author | Viswanathan, Arjun | |
| dc.contributor.author | Zohar, Yoni | |
| dc.contributor.author | Tinelli, Cesare | |
| dc.contributor.author | Barrett, Clark Stanford University, | |
| dc.date.accessioned | 2023-10-31T12:55:47Z | |
| dc.date.available | 2023-10-31T12:55:47Z | |
| dc.date.issued | 2023 | en_US |
| dc.identifier.citation | Ekici, B., Viswanathan, A., Zohar, Y., Tinelli, C., & Barrett, C. (2023, September). Formal Verification of Bit-Vector Invertibility Conditions in Coq. In International Symposium on Frontiers of Combining Systems (pp. 41-59). Cham: Springer Nature Switzerland. | en_US |
| dc.identifier.isbn | 978-303143368-9 | |
| dc.identifier.issn | 03029743 | |
| dc.identifier.uri | https://doi.org/10.1007/978-3-031-43369-6_3 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12809/11068 | |
| dc.description.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. | en_US |
| dc.item-language.iso | eng | en_US |
| dc.publisher | Springer Science and Business Media Deutschland GmbH | en_US |
| dc.relation.isversionof | 10.1007/978-3-031-43369-6_3 | en_US |
| dc.item-rights | info:eu-repo/semantics/openAccess | en_US |
| dc.subject | Invertibility conditions | en_US |
| dc.title | Formal Verification of Bit-Vector Invertibility Conditions in Coq | en_US |
| dc.item-type | article | en_US |
| dc.contributor.department | MÜ, Mühendislik Fakültesi, Bilgisayar Mühendisliği Bölümü | en_US |
| dc.contributor.authorID | 0000-0002-6602-7906 | en_US |
| dc.contributor.institutionauthor | Ekici, Burak | |
| dc.identifier.volume | 14279 | en_US |
| dc.identifier.startpage | 41 | en_US |
| dc.identifier.endpage | 59 | en_US |
| dc.relation.journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | en_US |
| dc.relation.publicationcategory | Konferans Öğesi - Uluslararası - Kurum Öğretim Elemanı | en_US |
