Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs

DOI10.1007/S10703-025-00476-3MaRDI QIDQ6903893zbMATH OpenFDO

Authors Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark Barrett

Publication date 7 November 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S10703-025-00476-3

zbMATH Keywords

compilersfinite fieldsSMTverificationzero-knowledge proofs

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Cites work

• A formally verified compiler back-end
• A mathematical introduction to logic.
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Isabelle/HOL. A proof assistant for higher-order logic
• Marlin: preprocessing zkSNARKs with universal and updatable SRS
• The knowledge complexity of interactive proof-systems
• The verified CakeML compiler backend
• Towards satisfiability modulo parametric bit-vectors

This page was built for publication: Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6903893)