{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:40:05Z","timestamp":1743061205543,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors\u2014used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5\u2014 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  library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions. \n<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_3","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"41-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of\u00a0Bit-Vector Invertibility Conditions in\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-7906","authenticated-orcid":false,"given":"Burak","family":"Ekici","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4464-8807","authenticated-orcid":false,"given":"Arjun","family":"Viswanathan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_8"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"3_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: A. Gupta & D. Kroening, editors: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"3_CR4","unstructured":"Beeren, J., et al.: Finite Machine Word Library. Archive of Formal Proofs. https:\/\/isa-afp.org\/entries\/Word Lib.html Formal proof development (2016)"},{"key":"3_CR5","unstructured":"Blot, A., Dagand, P.\u00c9., Lawall, J.: Bit Sequences and Bit Sets Library. Available at https:\/\/github.com\/pedagand\/ssrbit"},{"key":"3_CR6","unstructured":"Chajed, T., et al.: Bedrock Bit Vectors Library. Available at https:\/\/github.com\/mit-plv\/bbv"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1-4), pp. 423\u2013453 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9458-4","DOI":"10.1007\/s10817-018-9458-4"},{"key":"3_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7"},{"key":"3_CR9","unstructured":"Duprat, J.: Library Coq. Bool. Bvector. https:\/\/coq.inria.fr\/library\/Coq.Bool.Bvector.html"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126\u2013133. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Ekici, B., Viswanathan, A., Zohar, Y., Barrett, C.W., Tinelli, C.: Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). In Giselle Reis & Haniel Barbosa, editors: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019. EPTCS 301, pp. 18\u201326 (2019). https:\/\/doi.org\/10.4204\/EPTCS.301.4. Available at https:\/\/doi.org\/10.4204\/EPTCS.301.4","DOI":"10.4204\/EPTCS.301.4 10.4204\/EPTCS.301.4"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Herbert, B. Enderton (2001): Chapter TWO - First-Order Logic. In Herbert B. Enderton, editor: A Mathematical Introduction to Logic (Second Edition), second edition edition, Academic Press, Boston, pp. 67\u2013181, https:\/\/doi.org\/10.1016\/B978-0-08-049646-7.50008-4","DOI":"10.1016\/B978-0-08-049646-7.50008-4"},{"key":"3_CR13","unstructured":"Gupta, A., Fisher, A.L.: Representation and symbolic manipulation of linearly inductive boolean functions. In: Proceedings of the 1993 IEEE\/ACM International Conference on Computer-aided Design, ICCAD \u201993, IEEE Computer Society Press, Los Alamitos, CA, USA, pp. 192\u2013199 (1993). Available at http:\/\/dl.acm.org.stanford.idm.oclc.org\/citation.cfm?id=259794.259827"},{"key":"3_CR14","unstructured":"Niemetz, A., Preiner, M.: Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. In: FMCAD, IEEE, pp. 214\u2013224 (2020)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"issue":"7","key":"3_CR16","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/s10817-021-09598-9","volume":"65","author":"A Niemetz","year":"2021","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C.: Towards satisfiability modulo parametric bit-vectors. J. Autom. Reason. 65(7), 1001\u20131025 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09598-9","journal-title":"J. Autom. Reason."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-030-29436-6_22","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Niemetz","year":"2019","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C.: Towards bit-width-independent proofs in SMT Solvers. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 366\u2013384. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_22"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): 5. the rules of the game. In: Isabelle\/HOL. LNCS, vol. 2283, pp. 67\u2013104. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9_5","DOI":"10.1007\/3-540-45949-9_5"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328\u2013345. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0037116"},{"key":"3_CR20","unstructured":"Paulin-Mohring, C.: Introduction to the Calculus of Inductive Constructions. In: Bruno Woltzenlogel Paleo & David Delahaye, editors: All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations) 55, College Publications. https:\/\/hal.inria.fr\/hal-01094195 (2015)"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Paulsson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In: Sutcliffe, G., Schulz, S., Ternovska, E., eds: The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011, EPiC Series in Computing 2, EasyChair, pp. 1\u201311, https:\/\/doi.org\/10.29007\/36dt. Available at https:\/\/doi.org\/10.29007\/36dt","DOI":"10.29007\/36dt"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-81688-9_7","volume-title":"Computer Aided Verification","author":"X Shi","year":"2021","unstructured":"Shi, X., Fu, Y.-F., Liu, J., Tsai, M.-H., Wang, B.-Y., Yang, B.-Y.: CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 149\u2013171. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_7"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Sozeau, M.: Equations: A dependent pattern-matching compiler. In: Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), pp. 419\u2013434 (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_29","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Spies, S., Forster, Y.: Undecidability of higher-order unification formalised in Coq. In: Blanchette, J., Hritcu, C., eds.: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20\u201321, 2020, ACM, pp. 143\u2013157, https:\/\/doi.org\/10.1145\/3372885.3373832. Available at https:\/\/doi.org\/10.1145\/3372885.3373832","DOI":"10.1145\/3372885.3373832 10.1145\/3372885.3373832"},{"key":"3_CR25","unstructured":"The Coq development team (2019): The Coq Proof Assistant Reference Manual Version 8.9. Available at https:\/\/coq.inria.fr\/distrib\/current\/refman\/"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43369-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:31Z","timestamp":1694701951000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}