{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:50:15Z","timestamp":1762509015111,"version":"3.40.3"},"publisher-location":"Cham","reference-count":102,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377020"},{"type":"electronic","value":"9783031377037"}],"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,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"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 study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we construct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evaluate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors).<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_8","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"163-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Satisfiability Modulo Finite Fields"],"prefix":"10.1007","author":[{"given":"Alex","family":"Ozdemir","sequence":"first","affiliation":[]},{"given":"Gereon","family":"Kremer","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"8_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":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abbott, J., Bigatti, A.M., Palezzato, E., Robbiano, L.: Computing and using minimal polynomials. J. Symbolic Comput. 100 (2020)","DOI":"10.1016\/j.jsc.2019.07.022"},{"key":"8_CR3","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 in Programm. 119 (2021)","DOI":"10.1016\/j.jlamp.2020.100633"},{"key":"8_CR4","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":"8_CR5","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":"8_CR6","doi-asserted-by":"crossref","unstructured":"Aubry, P., Lazard, D., Maza, M.M.: On the theories of triangular sets. J. Symbolic Comput. 28(1) (1999)","DOI":"10.1006\/jsco.1999.0269"},{"key":"8_CR7","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":"8_CR8","unstructured":"Barlow, R.: Computational thinking breaks a logjam. https:\/\/www.bu.edu\/cise\/computational-thinking-breaks-a-logjam\/ (2015)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO (2005)","DOI":"10.1007\/11804192_17"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Barrett, C., et al.: CVC4. In: CAV (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0747-7171(92)90024-X","volume":"14","author":"D Bayer","year":"1992","unstructured":"Bayer, D., Stillman, M.: Computation of hilbert functions. J. Symb. Comput. 14(1), 31\u201350 (1992)","journal-title":"J. Symb. Comput."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Bayless, S., Bayless, N., Hoos, H., Hu, A.: SAT modulo monotonic theories. In: AAAI (2015)","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"8_CR13","unstructured":"Baylina, J.: Circom. https:\/\/github.com\/iden3\/circom"},{"key":"8_CR14","unstructured":"bellman. https:\/\/github.com\/zkcrypto\/bellman"},{"key":"8_CR15","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media (2013)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Blum, M., Feldman, P., Micali, S.: Non-interactive zero-knowledge and its applications. In: Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, pp. 103\u2013112 (1988)","DOI":"10.1145\/62212.62222"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Bogetoft, P., et al.: Secure multiparty computation goes live. In: FC (2009)","DOI":"10.1007\/978-3-642-03549-4_20"},{"issue":"3\u20134","key":"8_CR18","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":"8_CR19","doi-asserted-by":"crossref","unstructured":"Braun, D., Magaud, N., Schreck, P.: Formalizing some \"small\" 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":"8_CR20","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: TACAS (2010)","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"8_CR21","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":"8_CR22","doi-asserted-by":"crossref","unstructured":"Campanelli, M., Gennaro, R., Goldfeder, S., Nizzardo, L.: Zero-knowledge contingent payments revisited: Attacks and payments for services. In: CCS (2017)","DOI":"10.1145\/3133956.3134060"},{"key":"8_CR23","unstructured":"Caviness, B.F., Johnson, J.R.: Quantifier elimination and cylindrical algebraic decomposition. Springer Science & Business Media (2012)"},{"key":"8_CR24","unstructured":"Chin, C., Wu, H., Chu, R., Coglio, A., McCarthy, E., Smith, E.: Leo: A programming language for formally verified, zero-knowledge applications. Cryptology ePrint Archive (2021)"},{"key":"8_CR25","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. In: ACM TOCL 19(3) (2018)","DOI":"10.1145\/3230639"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: TACAS (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: Smt-based verification of hybrid systems. In: AAAI (2012)","DOI":"10.1007\/s10703-012-0158-0"},{"key":"8_CR28","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":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","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. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26"},{"key":"8_CR30","unstructured":"Cox, D., Little, J., OShea, D.: Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer Science & Business Media (2013)"},{"key":"8_CR31","unstructured":"Davenport, J.: The axiom system (1992)"},{"key":"8_CR32","unstructured":"developers, M.: Monero technical specs. https:\/\/monerodocs.org\/technical-specs\/ (2022)"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"D\u2019silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Design Integr. Circ. Syst. 27(7) (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"key":"8_CR34","unstructured":"Dummit, D.S., Foote, R.M.: Abstract algebra, vol. 3. Wiley Hoboken (2004)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Eberhardt, J., Tai, S.: ZoKrates\u2013scalable privacy-preserving off-chain computations. In: IEEE Blockchain (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00199"},{"key":"8_CR37","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":"8_CR38","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":"8_CR39","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. Tech. rep, MIT (2018)"},{"key":"8_CR40","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 Oper. Syst. Rev. 54(1) (2020)","DOI":"10.1145\/3421473.3421477"},{"key":"8_CR41","unstructured":"Faug\u00e8re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases without reduction to zero (F5). In: ISSAC. ACM (2002)"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Faugere, J.C., Gianni, P., Lazard, D., Mora, T.: Efficient computation of zero-dimensional Gr\u00f6bner bases by change of ordering. J. Symb. Comput. 16(4) (1993)","DOI":"10.1006\/jsco.1993.1051"},{"issue":"1","key":"8_CR43","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":"8_CR44","unstructured":"Finance, Y.: Monero quote. https:\/\/finance.yahoo.com\/quote\/XMR-USD\/ (2022) Accessed 30 June 2022"},{"key":"8_CR45","unstructured":"Finance, Y.: Zcash quote. https:\/\/finance.yahoo.com\/quote\/ZEC-USD\/ (2022). Accessed 30 June 2022"},{"key":"8_CR46","unstructured":"Frankle, J., Park, S., Shaar, D., Goldwasser, S., Weitzner, D.: Practical accountability of secret processes. In: USENIX Security (2018)"},{"key":"8_CR47","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 Modeling and Comput. 1(3\u20134) (2006)","DOI":"10.3233\/SAT190012"},{"key":"8_CR48","unstructured":"Gao, S.: Counting zeros over finite fields with Gr\u00f6bner bases. Ph.D. thesis, Master\u2019s thesis, Carnegie Mellon University (2009)"},{"key":"8_CR49","unstructured":"GAP \u2013 Groups, Algorithms, and Programming, Version 4.13dev. www.gap-system.org (this year)"},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems. In: STOC (1985)","DOI":"10.1145\/22145.22178"},{"key":"8_CR51","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":"8_CR52","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":"8_CR53","unstructured":"Grubbs, P., Arun, A., Zhang, Y., Bonneau, J., Walfish, M.: $$\\{$$Zero-Knowledge$$\\}$$ middleboxes. In: USENIX Security (2022)"},{"key":"8_CR54","unstructured":"Hader, T.: Non-Linear SMT-Reasoning over Finite Fields. Ph.D. thesis, TU Wien (2022), mS Thesis"},{"key":"8_CR55","unstructured":"Hader, T., Kov\u00e1cs, L.: Non-linear SMT-reasoning over finite fields. In: SMT (2022). http:\/\/ceur-ws.org\/Vol-3185\/extended3245.pdf extended Abstract"},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Heath, D., Kolesnikov, V.: Stacked garbling for disjunctive zero-knowledge proofs. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques (2020)","DOI":"10.1007\/978-3-030-45727-3_19"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Heath, L.S., Loehr, N.A.: New algorithms for generating conway polynomials over finite fields. J. Symb. Comput. (2004)","DOI":"10.1016\/j.jsc.2004.03.002"},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"Heck, A., Koepf, W.: Introduction to MAPLE, vol. 1993 (1993)","DOI":"10.1007\/978-1-4684-0519-4"},{"key":"8_CR59","unstructured":"Hopwood, D., Bowe, S., Hornby, T., Wilcox, N.: Zcash protocol specification. https:\/\/raw.githubusercontent.com\/zcash\/zips\/master\/protocol\/protocol.pdf (2016)"},{"key":"8_CR60","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":"8_CR61","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., De Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4) (2013)","DOI":"10.1145\/2429135.2429155"},{"key":"8_CR62","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":"8_CR63","doi-asserted-by":"crossref","unstructured":"Kamara, S., Moataz, T., Park, A., Qin, L.: A decentralized and encrypted national gun registry. In: IEEE S &P (2021)","DOI":"10.1109\/SP40001.2021.00072"},{"key":"8_CR64","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-aided reasoning: ACL2 case studies, vol. 4. Springer Science & Business Media (2013)"},{"key":"8_CR65","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":"8_CR66","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":"8_CR67","doi-asserted-by":"crossref","unstructured":"Lazard, D.: A new method for solving algebraic systems of positive dimension. Discr. Appl. Math. 33, 1\u20133 (1991)","DOI":"10.1016\/0166-218X(91)90113-B"},{"issue":"2","key":"8_CR68","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0747-7171(08)80086-7","volume":"13","author":"D Lazard","year":"1992","unstructured":"Lazard, D.: Solving zero-dimensional algebraic systems. J. Symb. Comput. 13(2), 117\u2013131 (1992)","journal-title":"J. Symb. Comput."},{"key":"8_CR69","unstructured":"libsnark. https:\/\/github.com\/scipr-lab\/libsnark"},{"key":"8_CR70","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":"8_CR71","unstructured":"McEliece, R.J.: Finite fields for computer scientists and engineers, vol. 23. Springer Science & Business Media (2012)"},{"key":"8_CR72","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."},{"key":"8_CR73","unstructured":"Moura, L.d., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: TACAS (2008)"},{"key":"8_CR74","unstructured":"Moura, L.d., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: VMCAI (2013)"},{"key":"8_CR75","unstructured":"Moura, L.d., Kong, S., Avigad, J., Doorn, F.v., Raumer, J.v.: The lean theorem prover (system description). In: CADE (2015)"},{"key":"8_CR76","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. arXiv:2006.01621 (2020)"},{"key":"8_CR77","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: CAV (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"8_CR78","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM (2006)","DOI":"10.1145\/1217856.1217859"},{"key":"8_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR80","unstructured":"Noir. https:\/\/noir-lang.github.io\/book\/index.html"},{"key":"8_CR81","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":"8_CR82","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.: Satisfiability modulo finite fields (2023), https:\/\/eprint.iacr.org\/2023\/091, (Full version)","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"8_CR83","unstructured":"Parker, R.: Finite fields and conway polynomials (1990), talk at the IBM Heidelberg Scientific Center. Cited by Scheerhorn"},{"issue":"2","key":"8_CR84","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/2856449","volume":"59","author":"B Parno","year":"2016","unstructured":"Parno, B., Howell, J., Gentry, C., Raykova, M.: Pinocchio: nearly practical verifiable computation. Commun. ACM 59(2), 103\u2013112 (2016)","journal-title":"Commun. ACM"},{"key":"8_CR85","unstructured":"Philipoom, J.: Correct-by-construction finite field arithmetic in Coq. Ph.D. thesis, Massachusetts Institute of Technology (2018)"},{"key":"8_CR86","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: TACAS (1998)","DOI":"10.1007\/BFb0054170"},{"key":"8_CR87","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Probabilistic algorithms in finite fields. SIAM Journal on computing 9(2) (1980)","DOI":"10.1137\/0209024"},{"key":"8_CR88","doi-asserted-by":"publisher","unstructured":"Rabinowitsch, J.L.: Zum hilbertschen nullstellensatz. Mathematische Annalen 102 (1930), https:\/\/doi.org\/10.1007\/BF01782361","DOI":"10.1007\/BF01782361"},{"key":"8_CR89","unstructured":"Sasson, E.B., et al.: Zerocash: Decentralized anonymous payments from bitcoin. In: IEEE S &P (2014)"},{"key":"8_CR90","doi-asserted-by":"publisher","DOI":"10.1007\/BF01268660","volume-title":"Trace-and Norm-compatible Extensions of Finite Fields","author":"A Scheerhorn","year":"1992","unstructured":"Scheerhorn, A.: Trace-and Norm-compatible Extensions of Finite Fields. Applicable Algebra in Engineering, Communication and Computing (1992)"},{"key":"8_CR91","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":"8_CR92","doi-asserted-by":"crossref","unstructured":"Setty, S., Braun, B., Vu, V., Blumberg, A.J., Parno, B., Walfish, M.: Resolving the conflict between generality and plausibility in verified computation. In: Proceedings of the 8th ACM European Conference on Computer Systems, pp. 71\u201384 (2013)","DOI":"10.1145\/2465351.2465359"},{"key":"8_CR93","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Automated deduction for verification. CSUR 41(4) (2009)","DOI":"10.1145\/1592434.1592437"},{"key":"8_CR94","doi-asserted-by":"crossref","unstructured":"Thaler, J.: Proofs, Arguments, and Zero-Knowledge (2022)","DOI":"10.1561\/9781638281252"},{"key":"8_CR95","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: PLDI (2014)","DOI":"10.1145\/2594291.2594340"},{"key":"8_CR96","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"},{"key":"8_CR97","unstructured":"Vella, L., Alt, L.: On satisfiability of polynomial equations over large prime field. In: SMT (2022). http:\/\/ceur-ws.org\/Vol-3185\/extended9913.pdf extended Abstract"},{"key":"8_CR98","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra-the quadratic case and beyond. Appl. Algebra Eng., Commun. Comput. 8(2) (1997)","DOI":"10.1007\/s002000050055"},{"key":"8_CR99","unstructured":"Wen-Ts\u00fan, W.: A zero structure theorem for polynomial-equations-solving and its applications. In: European Conference on Computer Algebra (1987)"},{"key":"8_CR100","unstructured":"Wolfram, S.: Mathematica: a system for doing mathematics by computer. Addison Wesley Longman Publishing Co., Inc. (1991)"},{"key":"8_CR101","unstructured":"Zimmermann, P., et al.: Computational mathematics with SageMath. SIAM (2018)"},{"key":"8_CR102","unstructured":"Zinc. https:\/\/zinc.matterlabs.dev\/"}],"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-37703-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:03:43Z","timestamp":1693047823000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":102,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_8","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":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}