{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:23:00Z","timestamp":1762816980285,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":27,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819542123","type":"print"},{"value":"9789819542130","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_12","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:12Z","timestamp":1762816692000},"page":"209-227","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ZK-ProVer: Proving Programming Verification in\u00a0Non-interactive Zero-Knowledge Proofs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-8367-9437","authenticated-orcid":false,"given":"Haoyu","family":"Wei","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6848-3105","authenticated-orcid":false,"given":"Jingyu","family":"Ke","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2698-1836","authenticated-orcid":false,"given":"Ruibang","family":"Liu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-7112","authenticated-orcid":false,"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Rao, A., Wang, Y.: Formal verification of autonomous vehicles: bridging the gap between model-based design and model checking. SAE Int. J. Adv. Curr. Pract. Mob. 6(2), 814\u2013826 (2024). https:\/\/doi.org\/10.4271\/2023-01-0116. https:\/\/www.sae.org\/publications\/technical-papers\/content\/2023-01-0116\/","DOI":"10.4271\/2023-01-0116"},{"issue":"8","key":"12_CR2","doi-asserted-by":"publisher","first-page":"166","DOI":"10.14569\/IJACSA.2018.090822","volume":"9","author":"Y Zhang","year":"2018","unstructured":"Zhang, Y., Wen, S., Xu, C.: Blockchain-based certificate verification system using smart contracts. Int. J. Adv. Comput. Sci. Appl. 9(8), 166\u2013171 (2018). https:\/\/doi.org\/10.14569\/IJACSA.2018.090822","journal-title":"Int. J. Adv. Comput. Sci. Appl."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-63406-3_13","volume-title":"Formal Methods and Software Engineering","author":"S Sarswat","year":"2020","unstructured":"Sarswat, S., Singh, A.K.: Formally verified trades in financial markets. In: Lin, S.-W., Hou, Z., Mahony, B. (eds.) ICFEM 2020. LNCS, vol. 12531, pp. 217\u2013232. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63406-3_13"},{"issue":"7","key":"12_CR4","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Biere, A., et al.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th Annual Design Automation Conference, pp. 317\u2013320. ACM (1999). https:\/\/doi.org\/10.1145\/309847.309942","DOI":"10.1145\/309847.309942"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-27940-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KRM Leino","year":"2012","unstructured":"Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315\u2013331. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_21"},{"issue":"3","key":"12_CR7","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1145\/116825.116852","volume":"38","author":"O Goldreich","year":"1991","unstructured":"Goldreich, O., Micali, S., Wigderson, A.: Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems. J. ACM 38(3), 690\u2013728 (1991). https:\/\/doi.org\/10.1145\/116825.116852","journal-title":"J. ACM"},{"key":"12_CR8","unstructured":"Dokchitser, T., Bulkin, A.: Zero knowledge virtual machine step by step. Cryptology ePrint Archive, Paper 2023\/1032 (2023). https:\/\/eprint.iacr.org\/2023\/1032"},{"key":"12_CR9","unstructured":"Gabizon, A., Williamson, Z.J., Ciobotaru, O.: PLONK: permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge. Cryptology ePrint Archive, Paper 2019\/953 (2019). https:\/\/eprint.iacr.org\/2019\/953"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Chen, B., et al.: HyperPlonk: plonk with linear-time prover and high- degree custom gates (2022). ePrint: 2022\/1355 (IACR Cryptology)","DOI":"10.1007\/978-3-031-30617-4_17"},{"key":"12_CR11","series-title":"Technology, Work and Globalization","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-031-51063-2_8","volume-title":"Human Privacy in Virtual and Physical Worlds","author":"KK Garimella","year":"2024","unstructured":"Garimella, K.K., Conway, D.: Zero-knowledge proofs and privacy: a technical look at privacy. In: Lacity, M.C., Coon, L. (eds.) Human Privacy in Virtual and Physical Worlds. TWG, pp. 157\u2013179. Palgrave Macmillan, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-51063-2_8"},{"issue":"12","key":"12_CR12","doi-asserted-by":"publisher","first-page":"5005","DOI":"10.3390\/app14125005","volume":"14","author":"J Guo","year":"2024","unstructured":"Guo, J., et al.: Efficient and secure EMR storage and sharing scheme based on hyperledger fabric and IPFS. Appl. Sci. 14(12), 5005 (2024)","journal-title":"Appl. Sci."},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/978-3-642-38348-9_37","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2013","author":"R Gennaro","year":"2013","unstructured":"Gennaro, R., Gentry, C., Parno, B., Raykova, M.: Quadratic span programs and succinct NIZKs without PCPs. In: Johansson, T., Nguyen, P.Q. (eds.) EUROCRYPT 2013. LNCS, vol. 7881, pp. 626\u2013645. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38348-9_37"},{"key":"12_CR14","unstructured":"Polytope Research. Verkle Trees (2025). https:\/\/research.polytope.technology\/verkle-trees. Accessed 14 June 2025"},{"issue":"6","key":"12_CR15","doi-asserted-by":"publisher","first-page":"4508","DOI":"10.1109\/TSC.2024.3422798","volume":"17","author":"S Gao","year":"2024","unstructured":"Gao, S., Li, G., Fu, H.: ZKWASM: a ZKSNARKWASM emulator. IEEE Trans. Serv. Comput. 17(6), 4508\u20134521 (2024). https:\/\/doi.org\/10.1109\/TSC.2024.3422798","journal-title":"IEEE Trans. Serv. Comput."},{"key":"12_CR16","unstructured":"Bowe, S., Grigg, J., Hopwood, D.: Recursive proof composition without a trusted setup. Cryptology ePrint Archive, Paper 2019\/1021 (2019). https:\/\/eprint.iacr.org\/2019\/1021"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Parno, B., et al.: Pinocchio: nearly practical verifiable computation. In: Proceedings of the IEEE Symposium on Security and Privacy. Best Paper Award, pp. 238\u2013252. IEEE (2013). https:\/\/eprint.iacr.org\/2013\/279.pdf","DOI":"10.1109\/SP.2013.47"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Wahby, R.S., et al.: Full accounting for verifiable outsourcing. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2071\u20132086. ACM (2017). https:\/\/eprint.iacr.org\/2017\/242.pdf","DOI":"10.1145\/3133956.3133984"},{"key":"12_CR20","unstructured":"Setty, S.T.V., et al.: Making argument systems for outsourced computation practical (sometimes). In: Proceedings of the Network and Distributed System Security Symposium (NDSS). The Internet Society (2012)"},{"key":"12_CR21","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Design, Automation and Test in Europe Conference (DATE), pp. 10880\u201310885. IEEE (2003). https:\/\/www.princeton.edu\/~chaff\/publication\/DATE2003_validating_sat_solver.pdf"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-40084-1_6","volume-title":"Advances in Cryptology \u2013 CRYPTO 2013","author":"E Ben-Sasson","year":"2013","unstructured":"Ben-Sasson, E., Chiesa, A., Genkin, D., Tromer, E., Virza, M.: SNARKs for C: verifying program executions succinctly and in zero knowledge. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013. LNCS, vol. 8043, pp. 90\u2013108. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40084-1_6"},{"key":"12_CR24","unstructured":"StarkWare. Cairo \u2013 a Turing-complete STARK-friendly CPU architecture. Technical Report. StarkWare technical documentation (2021). https:\/\/eprint.iacr.org\/2021\/1063"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Luo, N., et al.: Proving UNSAT in zero knowledge. In: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2203\u20132217. ACM (2022). https:\/\/doi.org\/10.1145\/3548606.3559373","DOI":"10.1145\/3548606.3559373"},{"key":"12_CR26","unstructured":"Luick, D., et al.: ZKSMT: a VM for proving SMT theorems in zero knowledge. In: 33rd USENIX Security Symposium (USENIX Security 2024), pp. 3837\u20133845 (2024)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Fang, Z., et al.: Zero knowledge static program analysis. In: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2271\u20132288. ACM (2021). https:\/\/david.darais.com\/assets\/papers\/zk-sa\/zk-sa.pdf","DOI":"10.1145\/3460120.3484795"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:14Z","timestamp":1762816694000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}