{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:39Z","timestamp":1784837799253,"version":"3.55.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Satisfiability modulo finite fields enables automated verification for cryptosystems. Unfortunately, previous solvers scale poorly for even some simple systems of field equations, in part because they build a full Gr\u00f6bner basis (GB) for the system. We propose a new solver that uses multiple, simpler GBs instead of one full GB. Our solver, implemented within the cvc5 SMT solver, admits specialized propagation algorithms, e.g., for understanding bitsums. Experiments show that it solves important bitsum-heavy determinism benchmarks far faster than prior solvers, without introducing much overhead for other benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_1","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"3-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Split Gr\u00f6bner Bases for\u00a0Satisfiability Modulo Finite Fields"],"prefix":"10.1007","author":[{"given":"Alex","family":"Ozdemir","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shankara","family":"Pailoor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alp","family":"Bassa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kostas","family":"Ferles","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"I\u015fil","family":"Dillig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"1_CR1","unstructured":"0xPARC. ZK bug tracker. https:\/\/github.com\/0xPARC\/zk-bug-tracker. Accessed 5 Sept 2023, via archive.org"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, B., McGrew, D.: TLS beyond the browser: Combining end host and network data to understand application behavior. In: IMC (2019)","DOI":"10.1145\/3355369.3355601"},{"key":"1_CR3","unstructured":"Archer, D., O\u2019Hara, A., Issa, R., Strauss, S.: Sharing sensitive department of education data across organizational boundaries using secure multiparty computation (2021)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"1_CR5","unstructured":"Barlow, R.: Computational thinking breaks a logjam (2015). https:\/\/www.bu.edu\/cise\/computational-thinking-breaks-a-logjam\/"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Bell\u00e9s-Mu\u00f1oz, M., Isabel, M., Mu\u00f1oz-Tapia, J.L., Rubio, A., Baylina, J.: Circom: a circuit description language for building zero-knowledge applications. IEEE Trans. Dependable Secure Comput. (2022)","DOI":"10.1109\/TDSC.2022.3232813"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bogetoft, P., et\u00a0al.: Secure multiparty computation goes live. In: FC (2009)","DOI":"10.1007\/978-3-642-03549-4_20"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Braun, D., Magaud, N., Schreck, P.: Formalizing some \u201csmall\u201d finite models of projective geometry in coq. In: International Conference on Artificial Intelligence and Symbolic Computation (2018)","DOI":"10.1007\/978-3-319-99957-9_4"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. SIGSAM Bulletin (1976)","DOI":"10.1145\/1088216.1088219"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"B\u00fcnz, B., Bootle, J., Boneh, D., Poelstra, A., Wuille, P., Maxwell, G.: Bulletproofs: Short proofs for confidential transactions and more. In: IEEE S&P (2018)","DOI":"10.1109\/SP.2018.00020"},{"key":"1_CR12","unstructured":"Chaliasos, S., Ernstberger, J., Theodore, D., Wong, D., Jahanara, M., Livshits, B.: Sok: what don\u2019t we know? understanding security vulnerabilities in snarks (2024). https:\/\/arxiv.org\/abs\/2402.15293"},{"key":"1_CR13","unstructured":"Chin, C., Wu, H., Chu, R., Coglio, A., McCarthy, E., Smith, E.: Leo: a programming language for formally verified, zero-knowledge applications (2021). Preprint at https:\/\/ia.cr\/2021\/651"},{"key":"1_CR14","volume-title":"Bosphorus: Bridging anf and cnf solvers","author":"D Choo","year":"2019","unstructured":"Choo, D., Soos, M., Chai, K.M.A., Meel, K.S.: Bosphorus: Bridging anf and cnf solvers. IEEE, In DATE (2019)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Coglio, A., McCarthy, E., Smith, E., Chin, C., Gaddamadugu, P., Dellepere, M.: Compositional formal verification of zero-knowledge circuits (2023). https:\/\/ia.cr\/2023\/1278","DOI":"10.4204\/EPTCS.393.9"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Pragmatic quotient types in coq. In: ITP (2013)","DOI":"10.1007\/978-3-642-39634-2_17"},{"key":"1_CR17","unstructured":"Cox, D., Little, J., OShea, D.:\u00a0Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer Science & Business Media (2013)"},{"key":"1_CR18","unstructured":"CVE-2014-3570. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2014-3570"},{"key":"1_CR19","unstructured":"CVE-2017-3732. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-3732"},{"key":"1_CR20","unstructured":"Dahlgren, F.: It pays to be Circomspect (2022). https:\/\/blog.trailofbits.com\/2022\/09\/15\/it-pays-to-be-circomspect\/. Accessed 15 Oct 2023"},{"key":"1_CR21","unstructured":"Dummit, D.S., Foote, R.M.: Abstract algebra, vol.\u00a03. Wiley Hoboken (2004)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Eberhardt, J., Tai, S.: ZoKrates\u2014scalable privacy-preserving off-chain computations. In: IEEE Blockchain (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00199"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A mathematical introduction to logic. Elsevier (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"1_CR25","volume-title":"Systematic generation of fast elliptic curve cryptography implementations","author":"A Erbsen","year":"2018","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Systematic generation of fast elliptic curve cryptography implementations. Technical report, MIT (2018)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic: With proofs, without compromises. ACM SIGOPS Operating Syst. Rev. 54(1) (2020)","DOI":"10.1145\/3421473.3421477"},{"key":"1_CR27","unstructured":"Y.\u00a0Finance. Monero quote (2023). https:\/\/finance.yahoo.com\/quote\/XMR-USD\/. Accessed 13 Oct 2023"},{"key":"1_CR28","unstructured":"Y.\u00a0Finance. Zcash quote (2023). https:\/\/finance.yahoo.com\/quote\/ZEC-USD\/. Accessed 13 Oct 2023"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Fournet, C., Keller, C., Laporte, V.: A certified compiler for verifiable computing. In: CSF (2016)","DOI":"10.1109\/CSF.2016.26"},{"key":"1_CR30","unstructured":"Gabizon, A., Williamson, Z.J., Ciobotaru, O.: Plonk: permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge (2019). https:\/\/ia.cr\/2019\/953"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: ITP, pp. 163\u2013179 (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"1_CR32","unstructured":"Greuel, G.-M., Pfister, G., Sch\u00f6nemann, H.: Singular-a computer algebra system for polynomial computations. In: Symbolic Computation and Automated Reasoning, pp. 227\u2013233. AK Peters\/CRC Press (2001)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Groth, J.: On the size of pairing-based non-interactive arguments. In: EUROCRYPT (2016)","DOI":"10.1007\/978-3-662-49896-5_11"},{"key":"1_CR34","unstructured":"Grubbs, P., Arun, A., Zhang, Y., Bonneau, J., Walfish, M.: Zero-knowledge middleboxes. In: USENIX Security (2022)"},{"key":"1_CR35","unstructured":"Hader, T.: Ffsat. https:\/\/github.com\/Ovascos\/ffsat, commit 67fecde"},{"key":"1_CR36","unstructured":"Hader, T.: Non-linear SMT-reasoning over finite fields (2022). MS Thesis (TU Wein)"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Hader, T., Kaufmann, D., Irfan, A., Graham-Lengrand, S., Kov\u00e1cs, L.: Mcsat-based finite field reasoning in the yices2 smt solver (2024)","DOI":"10.1007\/978-3-031-63498-7_23"},{"key":"1_CR38","unstructured":"Hader, T., Kaufmann, D., Kov\u00e1cs, L.: SMT solving over finite field arithmetic. In: LPAR (2023)"},{"key":"1_CR39","unstructured":"Hader, T., Kov\u00e1cs, L.: Non-linear SMT-reasoning over finite fields. In: SMT (2022). Extended Abstract"},{"key":"1_CR40","unstructured":"Hopwood, D., Bowe, S., Hornby, T., Wilcox, N.: Zcash protocol specification (2013). https:\/\/raw.githubusercontent.com\/zcash\/zips\/master\/protocol\/protocol.pdf"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Komendantsky, V., Konovalov, A., Linton, S.: View of computer algebra data from coq. In: International Conference on Intelligent Computer Mathematics (2011)","DOI":"10.1007\/978-3-642-22673-1_6"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Kotzias, P., Razaghpanah, A., Amann, J., Paterson, K.G., Vallina-Rodriguez, N., Caballero, J.: Coming of age: a longitudinal study of TLS deployment. In: IMC (2018)","DOI":"10.1145\/3278532.3278568"},{"key":"1_CR43","unstructured":"Liu, J., et al.: Certifying zero-knowledge circuits with refinement types (2023). https:\/\/ia.cr\/2023\/547"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-319-46520-3_27","volume-title":"Automated Technology for Verification and Analysis","author":"M Marescotti","year":"2016","unstructured":"Marescotti, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Clause sharing and partitioning for cloud-based SMT solving. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 428\u2013443. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_27"},{"issue":"3","key":"1_CR45","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"EW Mayr","year":"1982","unstructured":"Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305\u2013329 (1982)","journal-title":"Adv. Math."},{"key":"1_CR46","unstructured":"Monero technical specs (2022). https:\/\/monerodocs.org\/technical-specs\/"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to DPLL(T). J. ACM (2006)","DOI":"10.1145\/1217856.1217859"},{"key":"1_CR48","unstructured":"OpenSSL bug 1953. https:\/\/www.mail-archive.com\/openssl-dev@openssl.org\/msg23869.html"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Brown, F., Wahby, R.S.: CirC: compiler infrastructure for proof systems, software verification, and more. In: IEEE S&P (2022)","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.: Satisfiability modulo finite fields. In: CAV (2023)","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"1_CR51","unstructured":"Ozdemir, S., Pailoor, A.,\u00a0Bassa, A., Ferles, K., Barrett, C., Dillig, I.: Split Gr\u00f6bner bases for satisfiability modulo finite fields (2024). https:\/\/ia.cr\/2024\/572. Full version"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Wahby, R.S., Brown, F., Barrett, C.: Bounded verification for finite-field-blasting. In: CAV (2023)","DOI":"10.1007\/978-3-031-37709-9_8"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Pailoor, S., et al.: Automated detection of under-constrained circuits in zero-knowledge proofs. In: PLDI (2023)","DOI":"10.1145\/3591282"},{"key":"1_CR54","unstructured":"Philipoom, J.: Correct-by-construction finite field arithmetic in Coq. Ph.D. thesis, Massachusetts Institute of Technology (2018)"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Schwabe, P.,\u00a0Viguier, B., Weerwag, T., Wiedijk, F.: A coq proof of the correctness of x25519 in tweetnacl. In: CSF (2021)","DOI":"10.1109\/CSF51468.2021.00023"},{"key":"1_CR56","unstructured":"Soureshjani, F.H., Hall-Andersen, M., Jahanara, M., Kam, J., Gorzny, J., Ahmadvand, M.: Automated analysis of halo2 circuits (2023). https:\/\/ia.cr\/2023\/1051"},{"key":"1_CR57","unstructured":"Tornado.cash got hacked. by us (2019). https:\/\/tornado-cash.medium.com\/tornado-cash-got-hacked-by-us-b1e012a3c9a8. Accessed 13 Oct 2023"},{"key":"1_CR58","unstructured":"Wang, D.: Elimination methods. Springer Science & Business Media (2001)"},{"key":"1_CR59","unstructured":"Wang, F.: Ecne: automated verification of zk circuits (2022). https:\/\/0xparc.org\/blog\/ecne"},{"key":"1_CR60","unstructured":"Wen, H., et al.: Practical security analysis of zero-knowledge proof circuits (2023)"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/978-3-642-02658-4_60","volume-title":"Computer Aided Verification","author":"CM Wintersteiger","year":"2009","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 715\u2013720. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_60"},{"key":"1_CR62","unstructured":"Zcash counterfeiting vulnerability successfully remediated (2019). https:\/\/electriccoin.co\/blog\/zcash-counterfeiting-vulnerability-successfully-remediated\/. Accessed 13 Oct 2023"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:02:48Z","timestamp":1721934168000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}