{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T00:13:25Z","timestamp":1760832805838,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":84,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986673"},{"type":"electronic","value":"9783031986680"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a new refutation procedure\u00a0for multimodular systems of integer constraints that commonly arise\u00a0when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability\u00a0to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported\u00a0by algebraic tools like weighted Gr bner bases. Our experiments\u00a0show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related\u00a0to Montgomery arithmetic and zero-knowledge proofs.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_17","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:45:45Z","timestamp":1753130745000},"page":"339-362","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Integer Reasoning Modulo Different Constants in\u00a0SMT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9950-672X","authenticated-orcid":false,"given":"Elizaveta","family":"Pertseva","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0181-6752","authenticated-orcid":false,"given":"Alex","family":"Ozdemir","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9253-9585","authenticated-orcid":false,"given":"Shankara","family":"Pailoor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9685-7361","authenticated-orcid":false,"given":"Alp","family":"Bassa","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-5602","authenticated-orcid":false,"given":"Sorawee","family":"Porncharoenwase","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"I\u015fil","family":"Dillig","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":[[2025,7,22]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, J., Bigatti, A.M.: CoCoALib: A C++ library for computations in commutative algebra... and beyond. In: International Congress on Mathematical Software (2010)","DOI":"10.1007\/978-3-642-15582-6_15"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Logical Algebraic Methods Program. 119 (2021)","DOI":"10.1016\/j.jlamp.2020.100633"},{"key":"17_CR3","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":"17_CR4","doi-asserted-by":"crossref","unstructured":"Barreto, P.S., Lynn, B., Scott, M.: Constructing elliptic curves with prescribed embedding degrees. In: SCN (2003)","DOI":"10.1007\/3-540-36413-7_19"},{"key":"17_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"17_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":"17_CR7","unstructured":"Barrett, P.: Implementing the rivest shamir and adleman public key encryption algorithm on a standard digital signal processor. In: CRYPTO (1986)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Nachmanson, L.: Arithmetic solving in z3. In: CAV (2024)","DOI":"10.1007\/978-3-031-65627-9_2"},{"issue":"3\u20134","key":"17_CR9","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1006\/jsco.1996.0125","volume":"24","author":"W Bosma","year":"1997","unstructured":"Bosma, W., Cannon, J., Playoust, C.: The Magma algebra system I: the user language. J. Symb. Comput. 24(3\u20134), 235\u2013265 (1997)","journal-title":"J. Symb. Comput."},{"key":"17_CR10","unstructured":"Bowe, S.: BLS12-381: New zk-snark elliptic curve construction (Mar. 2017). https:\/\/electriccoin.co\/blog\/new-snark-curve\/"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: TACAS (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"17_CR12","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, University of Innsbruck (1965)"},{"key":"17_CR13","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":"17_CR14","unstructured":"Caviness, B.F., Johnson, J.R.: Quantifier elimination and cylindrical algebraic decomposition. Springer Science & Business Media (2012)"},{"key":"17_CR15","unstructured":"Chaliasos, S., Ernstberger, J., Theodore, D., Wong, D., Jahanara, M., and Livshits, B.: SoK: what don\u2019t we know? understanding security vulnerabilities in SNARKs. In: USENIX Security (2024)"},{"key":"17_CR16","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":"17_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM TOCL 19(3) (2018)","DOI":"10.1145\/3230639"},{"key":"17_CR18","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":"17_CR19","doi-asserted-by":"crossref","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. SAT (2015)","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"17_CR20","unstructured":"Dahlgren, F.: It pays to be Circomspect (2022). https:\/\/blog.trailofbits.com\/2022\/09\/15\/it-pays-to-be-circomspect\/. Accessed 15 October 2023"},{"key":"17_CR21","unstructured":"Davenport, J.: The axiom system (1992)"},{"key":"17_CR22","unstructured":"David, C.: Ideals, Varieties, and Algorithms-An Introduction to Computational Algebraic Geometry and Commutative Algebra. Undergraduate Texts in Mathematics (1991)"},{"key":"17_CR23","unstructured":"Decker, W., Greuel, G.-M., Pfister, G., Sch\u00f6nemann, H.: Singular 4-4-0 \u2014 A computer algebra system for polynomial computations (2024). http:\/\/www.singular.uni-kl.de"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inform. Theory 22(6) (1976)","DOI":"10.1109\/TIT.1976.1055638"},{"key":"17_CR25","unstructured":"Dummit, D.S., Foote, R.M.: Abstract algebra, vol.\u00a03. Wiley Hoboken (2004)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"17_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2019.10.020","volume":"103","author":"C Eder","year":"2021","unstructured":"Eder, C., Hofmann, T.: Efficient Gr\u00f6bner bases computation over principal ideal rings. J. Symb. Comput. 103, 1\u201313 (2021)","journal-title":"J. Symb. Comput."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Eisenbud, D., Grayson, D.R., Stillman, M., Sturmfels, B.: Computations in algebraic geometry with Macaulay 2, vol. 8. Springer Science & Business Media (2001)","DOI":"10.1007\/978-3-662-04851-1"},{"key":"17_CR29","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":"17_CR30","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Systematic generation of fast elliptic curve cryptography implementations. Technical report, MIT (2018)"},{"key":"17_CR31","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"},{"issue":"1","key":"17_CR32","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S0022-4049(99)00005-5","volume":"139","author":"JC Faug\u00e9re","year":"1999","unstructured":"Faug\u00e9re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases (f4). J. Pure Appl. Algebra 139(1), 61\u201388 (1999)","journal-title":"J. Pure Appl. Algebra"},{"key":"17_CR33","unstructured":"Faug\u00e9re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases without reduction to zero (f5). In: ISSAC. ACM (2002)"},{"key":"17_CR34","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":"17_CR35","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisfiability, Boolean Model. Comput. 1(3\u20134) (2006)","DOI":"10.3233\/SAT190012"},{"key":"17_CR36","unstructured":"GAP \u2013 Groups, Algorithms, and Programming, Version 4.13dev. https:\/\/www.gap-system.org, this year"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Gentry, C.: Fully homomorphic encryption using ideal lattices. In: STOC (2009)","DOI":"10.1145\/1536414.1536440"},{"issue":"1","key":"17_CR38","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1137\/0218012","volume":"18","author":"S Goldwasser","year":"1989","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof systems. SIAM J. Comput. 18(1), 186\u2013208 (1989)","journal-title":"SIAM J. Comput."},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"Graham-Lengrand, S., Jovanovi\u0107, D., Dutertre, B.: Solving bitvectors with MCSAT: explanations from bits and pieces. In: IJCAR (2020)","DOI":"10.1007\/978-3-030-51074-9_7"},{"key":"17_CR40","unstructured":"Hader, T.: Non-linear SMT-reasoning over finite fields. MS Thesis (TU Wein) (2022)"},{"key":"17_CR41","unstructured":"Hader, T., Kaufmann, D., Kov\u00e1cs, L.: SMT solving over finite field arithmetic. In: LPAR (2023)"},{"key":"17_CR42","unstructured":"Hader, T., Kov\u00e1cs, L.: Non-linear SMT-reasoning over finite fields. In: SMT. Extended Abstract (2022)"},{"key":"17_CR43","unstructured":"Hamburg, M.: Ed448-goldilocks, a new elliptic curve (2015).https:\/\/ia.cr\/2015\/625"},{"key":"17_CR44","doi-asserted-by":"crossref","unstructured":"Heck, A., Koepf, W.: Introduction to MAPLE, vol. 1993 (1993)","DOI":"10.1007\/978-1-4684-0519-4"},{"issue":"5","key":"17_CR45","first-page":"1038","volume":"48","author":"T Hickey","year":"2001","unstructured":"Hickey, T., Ju, Q., Van Emden, M.H.: Interval arithmetic: from principles to implementation. ACM 48(5), 1038\u20131068 (2001)","journal-title":"ACM"},{"key":"17_CR46","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: VMCAI (2017)","DOI":"10.1007\/978-3-319-52234-0_18"},{"key":"17_CR47","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., De\u00a0Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4) (2013)","DOI":"10.1145\/2429135.2429155"},{"key":"17_CR48","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Moura, L.d.: Cutting to the chase solving linear integer arithmetic. In: CADE (2011)","DOI":"10.1007\/978-3-642-22438-6_26"},{"key":"17_CR49","doi-asserted-by":"crossref","unstructured":"Kosba, A., Papamanthou, C., Shi, E.: xJsnark: A framework for efficient verifiable computation. In: IEEE S &P (2018)","DOI":"10.1109\/SP.2018.00018"},{"key":"17_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43"},{"key":"17_CR51","unstructured":"Liu, J., et al.: Certifying zero-knowledge circuits with refinement types (2023). https:\/\/ia.cr\/2023\/547"},{"key":"17_CR52","unstructured":"Makhorin, A.: GNU linear programming kit version 4.6.0 (2024). http:\/\/www.gnu.org\/software\/glpk\/glpk.html"},{"key":"17_CR53","doi-asserted-by":"crossref","unstructured":"Mar\u00e9chal, A., Fouilh\u00e9, A., King, T., Monniaux, D., P\u00e9rin, M.: Polyhedral approximation of multivariate polynomials using handelman\u2019s theorem. In: VMCAI (2016)","DOI":"10.1007\/978-3-662-49122-5_8"},{"key":"17_CR54","doi-asserted-by":"crossref","unstructured":"McCoy, N.H.: Rings and ideals, vol.\u00a08. American Mathematical Soc. (1948)","DOI":"10.5948\/9781614440086"},{"key":"17_CR55","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: Sympy: symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017)","journal-title":"PeerJ Comput. Sci."},{"issue":"170","key":"17_CR56","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1090\/S0025-5718-1985-0777282-X","volume":"44","author":"PL Montgomery","year":"1985","unstructured":"Montgomery, P.L.: Modular multiplication without trial division. Math. Comput. 44(170), 519\u2013521 (1985)","journal-title":"Math. Comput."},{"key":"17_CR57","unstructured":"Moura, L.d., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS (2008)"},{"key":"17_CR58","unstructured":"Moura, L.d., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: VMCAI (2013)"},{"key":"17_CR59","unstructured":"Niemetz, A., Preiner, M.: Ternary propagation-based local search for more bit-precise reasoning. In: FMCAD (2020)"},{"key":"17_CR60","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: CAV (2023)","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"17_CR61","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C.: Towards bit-width-independent proofs in SMT solvers. In: CADE (2019)","DOI":"10.1007\/978-3-030-29436-6_22"},{"key":"17_CR62","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Zohar, Y.: Scalable bit-blasting with abstractions. In: CAV (2024)","DOI":"10.1007\/978-3-031-65627-9_9"},{"issue":"3","key":"17_CR63","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1017\/S0004972700019973","volume":"64","author":"GH Norton","year":"2001","unstructured":"Norton, G.H., S\u01cel\u01cegean, A.: Strong Gr\u00f6bner bases for polynomials over a principal ideal ring. Bull. Aust. Math. Soc. 64(3), 505\u2013528 (2001)","journal-title":"Bull. Aust. Math. Soc."},{"key":"17_CR64","unstructured":"o1-labs. Foreign field multiplication gate (2024). https:\/\/github.com\/o1-labs\/rfcs\/blob\/eeb8070c9901c611c9a557464022bbf9237900b9\/0006-ffmul-revised.md"},{"key":"17_CR65","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":"17_CR66","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Pailoor, S., Bassa, A., Ferles, K., Barrett, C., Dillig, I.: Split Gr\u00f6bner Bases for satisfiability modulo finite fields. In: CAV (2024)","DOI":"10.1007\/978-3-031-65627-9_1"},{"key":"17_CR67","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":"17_CR68","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":"17_CR69","doi-asserted-by":"crossref","unstructured":"Pertseva, E., et al.: Integer reasoning modulo different constants in smt (2025). https:\/\/arxiv.org\/abs\/2505.14998","DOI":"10.1007\/978-3-031-98668-0_17"},{"key":"17_CR70","unstructured":"Philipoom, J.: Correct-by-construction finite field arithmetic in Coq PhD thesis, Massachusetts Institute of Technology (2018)"},{"key":"17_CR71","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: SC (1991)","DOI":"10.1145\/125826.125848"},{"issue":"2","key":"17_CR72","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"RL Rivest","year":"1978","unstructured":"Rivest, R.L., Shamir, A., Adleman, L.: A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21(2), 120\u2013126 (1978)","journal-title":"Commun. ACM"},{"key":"17_CR73","doi-asserted-by":"crossref","unstructured":"Schwabe, P., Viguier, 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":"17_CR74","doi-asserted-by":"crossref","unstructured":"Sheng, Y., et al.: Reasoning about vectors using an SMT theory of sequences. In: IJCAR (2022)","DOI":"10.1007\/978-3-031-10769-6_9"},{"key":"17_CR75","unstructured":"Succinct Labs. Gnark Plonky2 recursive verifier: The goldilocks field implementation (2024). https:\/\/github.com\/succinctlabs\/gnark-plonky2-verifier\/tree\/7025b2efd67b5ed30bd85f93c694774106d21b3d\/goldilocks"},{"key":"17_CR76","unstructured":"Tsay, C., Kronqvist, J., Thebelt, A., Misener, R.: Partition-based formulations for mixed-integer optimization of trained relu neural networks. NeurIPS (2021)"},{"key":"17_CR77","doi-asserted-by":"crossref","unstructured":"Tung, V.X., Khanh, T.V., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. In: IJCAR (2016)","DOI":"10.1007\/978-3-319-40229-1_16"},{"issue":"2","key":"17_CR78","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/2641562","volume":"58","author":"M Walfish","year":"2015","unstructured":"Walfish, M., Blumberg, A.J.: Verifying computations without reexecuting them. Commun. ACM 58(2), 74\u201384 (2015)","journal-title":"Commun. ACM"},{"key":"17_CR79","unstructured":"Wang, F.: Ecne: Automated verification of ZK circuits (2022). https:\/\/0xparc.org\/blog\/ecne"},{"key":"17_CR80","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2013the quadratic case and beyond. Applicable Algebra Eng. Commun. Comput. 8(2) (1997)","DOI":"10.1007\/s002000050055"},{"key":"17_CR81","unstructured":"Wen, H., et al.: Practical security analysis of zero-knowledge proof circuits (2023). https:\/\/ia.cr\/2023\/190"},{"key":"17_CR82","unstructured":"Wolfram, S.: Mathematica: a system for doing mathematics by computer. Addison Wesley Longman Publishing Co., Inc (1991)"},{"key":"17_CR83","doi-asserted-by":"crossref","unstructured":"Yao, A.C.: Protocols for secure computations. In: FOCS (1982)","DOI":"10.1109\/SFCS.1982.38"},{"key":"17_CR84","unstructured":"Zimmermann, P., et al.: Computational mathematics with SageMath. SIAM (2018)"}],"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-98668-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T05:38:30Z","timestamp":1760765910000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Shankara Pailoor, Alp Bassa, and Isil Dillig are employed at Veridise. Alex Ozdemir and Sorawee Porncharoenwase previously worked at Veridise. Sorawee Porncharoenwase is currently employed at Amazon Web Services (AWS). Clark Barrett is an Amazon Scholar.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}