{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T05:08:18Z","timestamp":1762492098625,"version":"build-2065373602"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:00:00Z","timestamp":1746230400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:00:00Z","timestamp":1746230400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2110397","2110397"],"award-info":[{"award-number":["2110397","2110397"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["SIEVE"],"award-info":[{"award-number":["SIEVE"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,11]]},"DOI":"10.1007\/s10703-025-00476-3","type":"journal-article","created":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:11:44Z","timestamp":1746263504000},"page":"161-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs"],"prefix":"10.1007","volume":"67","author":[{"given":"Alex","family":"Ozdemir","sequence":"first","affiliation":[]},{"given":"Riad S.","family":"Wahby","sequence":"additional","affiliation":[]},{"given":"Fraser","family":"Brown","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"key":"476_CR1","unstructured":"LLVM language reference manual. https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"476_CR2","unstructured":"Monero technical specs. https:\/\/monerodocs.org\/technical-specs\/ (2022)"},{"key":"476_CR3","unstructured":"Airscript. https:\/\/github.com\/0xPolygonMiden\/air-script"},{"key":"476_CR4","unstructured":"Angel S, Blumberg AJ, Ioannidis E, Woods J (2022) Efficient representation of numerical optimization problems for SNARKs. In: USENIX Security"},{"issue":"6","key":"476_CR5","doi-asserted-by":"publisher","first-page":"4733","DOI":"10.1109\/TDSC.2022.3232813","volume":"20","author":"M Bell\u00e9s-Mu\u00f1oz","year":"2022","unstructured":"Bell\u00e9s-Mu\u00f1oz M, Isabel M, Mu\u00f1oz-Tapia JL, Rubio A, Baylina J (2022) Circom: a circuit description language for building zero-knowledge applications. IEEE Trans Depend Secure Comput 20(6):4733\u20134751","journal-title":"IEEE Trans Depend Secure Comput"},{"key":"476_CR6","unstructured":"Bellman. https:\/\/github.com\/zkcrypto\/bellman"},{"key":"476_CR7","doi-asserted-by":"crossref","unstructured":"Ben-Sasson E, Bentov I, Horesh Y, Riabzev M (2019) Scalable zero knowledge with no trusted setup. In: CRYPTO","DOI":"10.1007\/978-3-030-26954-8_23"},{"key":"476_CR8","unstructured":"Bernstein DJ, Birkner P, Joye M, Lange T, Peters C (2008) Twisted edwards curves. In: AFRICACRYPT"},{"key":"476_CR9","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot Y, Cast\u00e9ran P (2013) Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media, UK"},{"key":"476_CR10","doi-asserted-by":"crossref","unstructured":"Blum M, Feldman P, Micali S (1988) Non-interactive zero-knowledge and its applications. In: STOC","DOI":"10.1145\/62212.62222"},{"key":"476_CR11","doi-asserted-by":"crossref","unstructured":"Brown F, Renner J, N\u00f6tzli A, Lerner S, Shacham H, Stefan D (2020) Towards a verified range analysis for JavaScript JITs. In: PLDI","DOI":"10.1145\/3395642"},{"key":"476_CR12","doi-asserted-by":"crossref","unstructured":"Campanelli M, Gennaro R, Goldfeder S, Nizzardo L (2017) Zero-knowledge contingent payments revisited: attacks and payments for services. In: CCS","DOI":"10.1145\/3133956.3134060"},{"key":"476_CR13","doi-asserted-by":"crossref","unstructured":"Chen E, Zhu J, Ozdemir A, Wahby RS, Brown F, Zheng W (2023) Silph: a framework for scalable and accurate generation of hybrid MPC protocols","DOI":"10.1109\/SP46215.2023.10179397"},{"key":"476_CR14","doi-asserted-by":"crossref","unstructured":"Chiesa A, Hu Y, Maller M, Mishra P, Vesely N, Ward N (2020) Marlin: preprocessing zkSNARKs with universal and updatable SRS. In: EUROCRYPT","DOI":"10.1007\/978-3-030-45721-1_26"},{"key":"476_CR15","unstructured":"Chin C, Wu H, Chu R, Coglio A, McCarthy E, Smith E (2021) Leo: a programming language for formally verified, zero-knowledge applications, Preprint at https:\/\/ia.cr\/2021\/651"},{"key":"476_CR16","doi-asserted-by":"crossref","unstructured":"Cowan M, Dangwal D, Alaghi A, Trippel C, Lee VT, Reagen B. (2021) Porcupine: a synthesizing compiler for vectorized homomorphic encryption. In: PLDI","DOI":"10.1145\/3453483.3454050"},{"key":"476_CR17","doi-asserted-by":"crossref","unstructured":"Eberhardt J, Tai S (2018) ZoKrates\u2014scalable privacy-preserving off-chain computations. In: IEEE Blockchain","DOI":"10.1109\/Cybermatics_2018.2018.00199"},{"key":"476_CR18","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"2001","unstructured":"Enderton HB (2001) A mathematical introduction to logic. Elsevier, UK"},{"key":"476_CR19","doi-asserted-by":"crossref","unstructured":"Fournet C, Keller C, Laporte V (2016) A certified compiler for verifiable computing. In: CSF","DOI":"10.1109\/CSF.2016.26"},{"key":"476_CR20","doi-asserted-by":"crossref","unstructured":"Fox A, Myreen MO, Tan YK, Kumar R (2017) Verified compilation of CakeML to multiple machine-code targets. In: CPP","DOI":"10.1145\/3018610.3018621"},{"key":"476_CR21","unstructured":"Frankle J, Park S, Shaar D, Goldwasser S, Weitzner D (2018) Practical accountability of secret processes. In: USENIX Security"},{"key":"476_CR22","unstructured":"Goldberg L, Papini S, Riabzev M (2021) Cairo\u2014a Turing-complete STARK-friendly CPU architecture, Preprint at https:\/\/ia.cr\/2021\/0163"},{"key":"476_CR23","doi-asserted-by":"crossref","unstructured":"Goldwasser S, Micali S, Rackoff C (1985) The knowledge complexity of interactive proof-systems. In: STOC","DOI":"10.1145\/22145.22178"},{"key":"476_CR24","unstructured":"Grubbs P, Arun A, Zhang Y, Bonneau J, Walfish M (2022) Zero-knowledge middleboxes. In: USENIX Security"},{"key":"476_CR25","unstructured":"Hopwood D, Bowe S, Hornby T, Wilcox N (2016) Zcash protocol specification. https:\/\/raw.githubusercontent.com\/zcash\/zips\/master\/protocol\/protocol.pdf"},{"key":"476_CR26","doi-asserted-by":"crossref","unstructured":"Jiang K, Chait-Roth D, DeStefano Z, Walfish M, Wies T (2023) Less is more: refinement proofs for probabilistic proofs. IEEE S &P","DOI":"10.1109\/SP46215.2023.10179393"},{"key":"476_CR27","doi-asserted-by":"crossref","unstructured":"Kamara S, Moataz T, Park A, Qin L (2021) A decentralized and encrypted national gun registry. In: IEEE S &P","DOI":"10.1109\/SP40001.2021.00072"},{"key":"476_CR28","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"M Kaufmann","year":"2013","unstructured":"Kaufmann M, Manolios P, Moore JS (2013) Computer-aided reasoning: ACL2 case studies, vol 4. Springer Science & Business Media, USA"},{"key":"476_CR29","unstructured":"Kosba A, Papadopoulos D, Papamanthou C, Song D (2020) MIRAGE: succinct arguments for randomized algorithms with applications to universal ZK-SNARKs. In: USENIX Security"},{"key":"476_CR30","doi-asserted-by":"crossref","unstructured":"Kosba A, Papamanthou C, Shi E (2018) xJsnark: a framework for efficient verifiable computation. In: IEEE S &P","DOI":"10.1109\/SP.2018.00018"},{"key":"476_CR31","unstructured":"Kothapalli A, Parno B (2022) Algebraic reductions of knowledge, Preprint at https:\/\/ia.cr\/2022\/009"},{"key":"476_CR32","doi-asserted-by":"crossref","unstructured":"Kumar R, Myreen MO, Norrish M, Owens S (2014) CakeML: a verified implementation of ML. In: POPL","DOI":"10.1145\/2535838.2535841"},{"key":"476_CR33","doi-asserted-by":"crossref","unstructured":"Kundu S, Tatlock Z, Lerner S (2009) Proving optimizations correct using parameterized program equivalence. In: PLDI","DOI":"10.1145\/1542476.1542513"},{"key":"476_CR34","unstructured":"Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO"},{"key":"476_CR35","doi-asserted-by":"crossref","unstructured":"Lerner S, Millstein T, Chambers C (2003) Automatically proving the correctness of compiler optimizations. In: PLDI","DOI":"10.1145\/781154.781156"},{"key":"476_CR36","doi-asserted-by":"crossref","unstructured":"Lerner S, Millstein T, Rice E, Chambers C (2005) Automated soundness proofs for dataflow analyses and transformations via local rules. In: POPL","DOI":"10.1145\/1040305.1040335"},{"issue":"7","key":"476_CR37","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"issue":"4","key":"476_CR38","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) A formally verified compiler back-end. J Autom Reason 43(4):363\u2013446","journal-title":"J Autom Reason"},{"key":"476_CR39","doi-asserted-by":"crossref","unstructured":"Lopes NP, Lee J, Hur CK, Liu Z, Regehr J (2021) Alive2: bounded translation validation for LLVM. In: PLDI","DOI":"10.1145\/3453483.3454030"},{"key":"476_CR40","doi-asserted-by":"crossref","unstructured":"Lopes NP, Menendez D, Nagarakatte S, Regehr J (2015) Provably correct peephole optimizations with Alive. In: PLDI","DOI":"10.1145\/2737924.2737965"},{"key":"476_CR41","doi-asserted-by":"crossref","unstructured":"Mullen E, Zuniga D, Tatlock Z, Grossman D (2016) Verified peephole optimizations for CompCert. In: PLDI","DOI":"10.1145\/2908080.2908109"},{"key":"476_CR42","doi-asserted-by":"crossref","unstructured":"Necula GC (2000) Translation validation for an optimizing compiler. In: PLDI","DOI":"10.1145\/349299.349314"},{"key":"476_CR43","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Reynolds A, Zohar Y, Barrett C, Tinelli C (2019) Towards bit-width-independent proofs in SMT solvers. In: CADE","DOI":"10.1007\/978-3-030-29436-6_22"},{"issue":"7","key":"476_CR44","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 (2021) Towards satisfiability modulo parametric bit-vectors. J Autom Reason 65(7):1001\u20131025","journal-title":"J Autom Reason"},{"key":"476_CR45","doi-asserted-by":"crossref","unstructured":"Nipkow T, Wenzel M, Paulson LC (2002) Isabelle\/HOL: a proof assistant for higher-order logic. Springer","DOI":"10.1007\/3-540-45949-9"},{"key":"476_CR46","unstructured":"Noir. https:\/\/noir-lang.github.io\/book\/index.html"},{"key":"476_CR47","doi-asserted-by":"crossref","unstructured":"Ozdemir A, Brown F, Wahby RS (2022) Circ: compiler infrastructure for proof systems, software verification, and more. In: IEEE S &P","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"476_CR48","doi-asserted-by":"crossref","unstructured":"Ozdemir A, Kremer G, Tinelli C, Barrett C (2023) Satisfiability modulo finite fields. In: CAV, Preprint at https:\/\/ia.cr\/2023\/091","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"476_CR49","unstructured":"Ozdemir A, Wahby R, Whitehat B, Boneh D (2020) Scaling verifiable computation using efficient set accumulators. In: USENIX Security"},{"key":"476_CR50","doi-asserted-by":"crossref","unstructured":"Ozdemir A, Wahby RS, Brown F, Barrett C (2023) Bounded verification for finite-field-blasting. In: CAV, (conference version)","DOI":"10.1007\/978-3-031-37709-9_8"},{"key":"476_CR51","doi-asserted-by":"crossref","unstructured":"Ozdemir A, Wahby RS, Brown F, Barrett C (2023) Bounded verification for finite-field-blasting. Cryptology ePrint Archive, https:\/\/ia.cr\/2023\/778, (Full version)","DOI":"10.1007\/978-3-031-37709-9_8"},{"issue":"2","key":"476_CR52","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 (2016) Pinocchio: nearly practical verifiable computation. Commun ACM 59(2):103\u2013112","journal-title":"Commun ACM"},{"key":"476_CR53","doi-asserted-by":"crossref","unstructured":"Pnueli A, Siegel M, Singerman E (1998) Translation validation. In: TACAS","DOI":"10.1007\/BFb0054170"},{"key":"476_CR54","unstructured":"Ranise S, Tinelli C, Barrett C (2017) SMT fixed size bit-vectors theory. https:\/\/smtlib.cs.uiowa.edu\/theories-FixedSizeBitVectors.shtml"},{"key":"476_CR55","unstructured":"Sasson EB, Chiesa A, Garman C, Green M, Miers I, Tromer E, Virza M (2014) Zerocash: decentralized anonymous payments from Bitcoin. In: IEEE S &P"},{"key":"476_CR56","doi-asserted-by":"crossref","unstructured":"Setty S, Braun B, Vu V, Blumberg AJ, Parno B, Walfish M (2013) Resolving the conflict between generality and plausibility in verified computation. In: EuroSys","DOI":"10.1145\/2465351.2465359"},{"key":"476_CR57","unstructured":"Snarky. https:\/\/github.com\/o1-labs\/snarky"},{"key":"476_CR58","doi-asserted-by":"crossref","unstructured":"Stewart G, Beringer L, Cuellar S, Appel AW (2015) Compositional CompCert. In: POPL","DOI":"10.1145\/2676726.2676985"},{"key":"476_CR59","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229","volume":"29","author":"YK Tan","year":"2019","unstructured":"Tan YK, Myreen MO, Kumar R, Fox A, Owens S, Norrish M (2019) The verified CakeML compiler backend. J Funct Programm 29:e2","journal-title":"J Funct Programm"},{"key":"476_CR60","doi-asserted-by":"crossref","unstructured":"Tao R, Shi Y, Yao J, Li X, Javadi-Abhari A, Cross AW, Chong FT, Gu R (2022) Giallar: push-button verification for the Qiskit quantum compiler. In: PLDI","DOI":"10.1145\/3519939.3523431"},{"key":"476_CR61","doi-asserted-by":"crossref","unstructured":"Thaler J (2022) Proofs, arguments, and zero-knowledge. Manuscript","DOI":"10.1561\/9781638281252"},{"key":"476_CR62","doi-asserted-by":"publisher","unstructured":"The Qiskit authors and maintainers: Qiskit: an open-source framework for quantum computing (2021). https:\/\/doi.org\/10.5281\/zenodo.2573505, The Qiskit maintainers request that the full list of Qiskit contributers be included in any citation. Regretfully, we cannot comply, as the list is two pages long","DOI":"10.5281\/zenodo.2573505"},{"key":"476_CR63","unstructured":"Tinelli C (2015) SMT core theory. https:\/\/smtlib.cs.uiowa.edu\/theories-Core.shtml"},{"key":"476_CR64","doi-asserted-by":"crossref","unstructured":"Viand A, Jattke P, Hithnawi A (2021) SoK: fully homomorphic encryption compilers. In: IEEE S &P","DOI":"10.1109\/SP40001.2021.00068"},{"key":"476_CR65","doi-asserted-by":"crossref","unstructured":"Wahby RS, Setty S, Howald M, Ren Z, Blumberg AJ, Walfish M (2015) Efficient RAM and control flow in verifiable outsourced computation. NDSS","DOI":"10.14722\/ndss.2015.23097"},{"issue":"2","key":"476_CR66","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/2641562","volume":"58","author":"M Walfish","year":"2015","unstructured":"Walfish M, Blumberg AJ (2015) Verifying computations without reexecuting them. Commun ACM 58(2):74\u201384","journal-title":"Commun ACM"},{"key":"476_CR67","unstructured":"Wang F (2022) Ecne: automated verification of ZK circuits https:\/\/0xparc.org\/blog\/ecne"},{"key":"476_CR68","unstructured":"Zinc. https:\/\/zinc.matterlabs.dev\/"},{"key":"476_CR69","doi-asserted-by":"crossref","unstructured":"Zohar Y, Irfan A, Mann M, Niemetz A, N\u00f6tzli A, Preiner M, Reynolds A, Barrett C, Tinelli C (2022) Bit-precise reasoning via int-blasting. In: CADE","DOI":"10.1007\/978-3-030-94583-1_24"},{"key":"476_CR70","unstructured":"ZoKrates. https:\/\/zokrates.github.io\/"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00476-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00476-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00476-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T05:03:26Z","timestamp":1762491806000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00476-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,3]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["476"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00476-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,5,3]]},"assertion":[{"value":"16 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}