{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:11Z","timestamp":1784793791641,"version":"3.55.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    At the core of modern electronic design automation (EDA) tools is\n                    <jats:italic>rewriting<\/jats:italic>\n                    : a mechanism by which local transformations are iteratively applied to circuits to make them faster and more efficient. These rewrites are crucial for producing high-quality hardware, and they often depend on extremely delicate conditions, relating, for example, to the widths of the various bitvectors involved. As such, it is both\n                    <jats:italic>desirable<\/jats:italic>\n                    and\n                    <jats:italic>difficult<\/jats:italic>\n                    to prove them correct. Prior work has studied the correctness of parametric-bitwidth rewrites in the context of software compilers and SMT solvers, but those approaches struggle to handle rewrites that have\n                    <jats:italic>multiple<\/jats:italic>\n                    bitwidth parameters, as are commonplace in EDA. We propose a language for expressing these multi-width parametric rewrites and provide a translation into equivalences in modular arithmetic. We then show how these equivalences can be automatically and efficiently proved using equality saturation over a set of carefully chosen axioms, and finally reconstructed automatically as theorems in Isabelle. This process is implemented in our solver, ParaBit. Using benchmarks from prior compilers work and from industrial EDA tools, we demonstrate that ParaBit can solve a class of problems that are intractable using existing techniques.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_20","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:18Z","timestamp":1784791038000},"page":"380-402","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Multi-width Parametric Bitvector Equivalence Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-2029-367X","authenticated-orcid":false,"given":"Luigi","family":"Rinaldi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7741-3271","authenticated-orcid":false,"given":"Samuel","family":"Coward","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"20_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). https:\/\/smt-lib.org\/"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Berger, Z., et al.: Bit-precise reasoning with parametric bit-vectors. In: Berg, J., Nordstr\u00f6m, J. (eds.) 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0341, pp. 4:1\u20134:24. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2025.4. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.SAT.2025.4","DOI":"10.4230\/LIPIcs.SAT.2025.4"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Bhat, S., Keizer, A., Hughes, C., Goens, A., Grosser, T.: Verifying peephole rewriting in SSA compiler IRs. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0309, pp. 9:1\u20139:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.9. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024.9","DOI":"10.4230\/LIPIcs.ITP.2024.9"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Bhat, S., Stefanesco, L., Hughes, C., Grosser, T.: Certified decision procedures for width-independent bitvector predicates. Proc. ACM Program. Lang. 9(OOPSLA2) (2025). https:\/\/doi.org\/10.1145\/3763148","DOI":"10.1145\/3763148"},{"key":"20_CR7","unstructured":"Cadence Design Systems: Jasper formal verification platform (2024). https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification.html"},{"key":"20_CR8","unstructured":"Cadence Design Systems: Genus synthesis solution (2026). https:\/\/www.cadence.com\/en_US\/home\/tools\/digital-design-and-signoff\/synthesis\/genus-synthesis-solution.html"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Cheng, J., Coward, S., Chelini, L., Barbalho, R., Drane, T.: SEER: super-optimization explorer for HLS using e-graph rewriting with MLIR. In: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 1029\u20131044. Association for Computing Machinery (2024). https:\/\/doi.org\/10.1145\/3620665.3640392","DOI":"10.1145\/3620665.3640392"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Coward, S., Constantinides, G.A., Drane, T.: Automatic datapath optimization using e-graphs. In: 2022 IEEE 29th Symposium on Computer Arithmetic (ARITH), pp. 43\u201350 (2022). https:\/\/doi.org\/10.1109\/ARITH54963.2022.00016","DOI":"10.1109\/ARITH54963.2022.00016"},{"key":"20_CR11","doi-asserted-by":"publisher","unstructured":"Coward, S., Drane, T., Constantinides, G.A.: Constraint-aware e-graph rewriting for hardware performance optimization. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 1\u201314 (2024). https:\/\/doi.org\/10.1109\/TCAD.2024.3483096","DOI":"10.1109\/TCAD.2024.3483096"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Coward, S., Drane, T., Constantinides, G.A.: ROVER: RTL optimization via verified e-graph rewriting. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 43, 4687\u20134700 (2024). https:\/\/doi.org\/10.1109\/TCAD.2024.3410154","DOI":"10.1109\/TCAD.2024.3410154"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Coward, S., Morini, E., Tan, B., Drane, T., Constantinides, G.: Datapath verification via word-level e-graph rewriting. In: Formal Methods in Computer-Aided Design (FMCAD) (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_17","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_17"},{"key":"20_CR14","unstructured":"Eldridge, S., et al.: MLIR as hardware compiler infrastructure. In: WOSET 2021: Workshop on Open Source EDA Technology (2021)"},{"key":"20_CR15","unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Formal Methods in Computer Aided Design, pp. 137\u2013144 (2010)"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, p.\u00a09. TU Wien Academic Press (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2-13","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2-13"},{"key":"20_CR17","unstructured":"Haftmann, F.: Theory bit operations (2025). https:\/\/isabelle.in.tum.de\/library\/HOL\/HOL\/Bit_Operations.html#Bit_Operations.semiring_bit_operations_class"},{"key":"20_CR18","doi-asserted-by":"publisher","unstructured":"Hou, T., Laddad, S., Hellerstein, J.M.: Towards relational contextual equality saturation (2025). https:\/\/doi.org\/10.48550\/arXiv.2507.11897","DOI":"10.48550\/arXiv.2507.11897"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"IEEE: IEEE Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language. Technical report, IEEE Std 1800-2023, IEEE (2023). https:\/\/doi.org\/10.1109\/IEEESTD.2024.10458102","DOI":"10.1109\/IEEESTD.2024.10458102"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Koelbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 196\u2013201. European Design and Automation Association (2009). https:\/\/doi.org\/10.1109\/DATE.2009.5090657","DOI":"10.1109\/DATE.2009.5090657"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, STOC 1977, pp. 164\u2013177. Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/800105.803406","DOI":"10.1145\/800105.803406"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Kurashige, C., et al.: CCLemma: E-graph guided lemma discovery for inductive equational proofs. Proc. ACM Program. Lang. 8, 818\u2013844 (2024). https:\/\/doi.org\/10.1145\/3674653","DOI":"10.1145\/3674653"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Lachnitt, H., et al.: IsaRare: automatic verification of SMT rewrites in Isabelle\/HOL. In: Tools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, 6\u201311 April 2024, Proceedings, Part I, pp. 311\u2013330. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_17","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Lee, J., Hur, C.K., Liu, Z., Regehr, J.: Alive2: bounded translation validation for LLVM. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 65\u201379. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"issue":"6","key":"20_CR25","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2813885.2737965","volume":"50","author":"NP Lopes","year":"2015","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with Alive. SIGPLAN Not. 50(6), 22\u201332 (2015). https:\/\/doi.org\/10.1145\/2813885.2737965","journal-title":"SIGPLAN Not."},{"key":"20_CR26","unstructured":"Micheli, G.D.: Synthesis and Optimization of Digital Circuits, 1st edn. McGraw-Hill Higher Education (1994)"},{"key":"20_CR27","unstructured":"de\u00a0Moura, L.: Lean grind tactic (2025). https:\/\/lean-lang.org\/doc\/reference\/latest\/The--grind--tactic\/"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Mukherjee, M., Regehr, J.: Hydra: generalizing peephole optimizations with program synthesis. Proc. ACM Program. Lang. 8(OOPSLA1) (2024). https:\/\/doi.org\/10.1145\/3649837","DOI":"10.1145\/3649837"},{"issue":"6","key":"20_CR31","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1145\/2980983.2908109","volume":"51","author":"E Mullen","year":"2016","unstructured":"Mullen, E., Zuniga, D., Tatlock, Z., Grossman, D.: Verified peephole optimizations for compcert. SIGPLAN Not. 51(6), 448\u2013461 (2016). https:\/\/doi.org\/10.1145\/2980983.2908109","journal-title":"SIGPLAN Not."},{"key":"20_CR32","unstructured":"Nelson, C.G.: Techniques for program verification. Ph.D. thesis, Stanford University, Stanford, CA, USA (1980)"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part II, pp. 3\u201317. Lecture Notes in Computer Science. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-030-29436-6_22","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Niemetz","year":"2019","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C.: Towards bit-width-independent proofs in SMT solvers. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 366\u2013384. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_22"},{"issue":"7","key":"20_CR35","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.: Towards satisfiability modulo parametric bit-vectors. J. Autom. Reason. 65(7), 1001\u20131025 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09598-9","journal-title":"J. Autom. Reason."},{"key":"20_CR36","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"20_CR37","doi-asserted-by":"publisher","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 1\u201311. Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737959","DOI":"10.1145\/2737924.2737959"},{"key":"20_CR38","doi-asserted-by":"publisher","unstructured":"Singher, E., Shachar, I.: Easter egg: equality reasoning based on e-graphs with multiple assumptions. In: Narodytska, N., R\u00fcmmer, P. (eds.) Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2024. Conference Series: Formal Methods in Computer-Aided Design, vol.\u00a05, pp. 70\u201383. TU Wien Academic Press (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_13","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_13"},{"key":"20_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737\u2013742. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_59"},{"key":"20_CR40","unstructured":"Synopsys: Design compiler (2026). https:\/\/www.synopsys.com\/implementation-and-signoff\/rtl-synthesis-test\/design-compiler.html"},{"key":"20_CR41","doi-asserted-by":"publisher","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM (JACM) 22 (1975). https:\/\/doi.org\/10.1145\/321879.321884","DOI":"10.1145\/321879.321884"},{"key":"20_CR42","doi-asserted-by":"publisher","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.\u00a044, pp. 264\u2013276. Association for Computing Machinery (2009). https:\/\/doi.org\/10.1145\/1480881.1480915","DOI":"10.1145\/1480881.1480915"},{"key":"20_CR43","doi-asserted-by":"publisher","unstructured":"Thomas, D.E., Moorby, P.R.: The Verilog Hardware Description Language, 5 edn. Springer, New York (2002). https:\/\/doi.org\/10.1007\/b116662","DOI":"10.1007\/b116662"},{"key":"20_CR44","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: Egg: fast and extensible equality saturation. In: Proceedings of the ACM on Principles of Programming Languages, vol.\u00a05. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"},{"key":"20_CR45","unstructured":"Wolf, C.: Yosys open synthesis suite. https:\/\/yosyshq.net\/yosys\/"},{"key":"20_CR46","unstructured":"Wolf, C.: SymbiYosys (sby) \u2013 front-end for Yosys-based formal verification flows (2017)"},{"key":"20_CR47","doi-asserted-by":"publisher","unstructured":"Zimmermann, R.: Datapath synthesis for standard-cell design. In: 19th IEEE Symposium on Computer Arithmetic, pp. 207\u2013211 (2009). https:\/\/doi.org\/10.1109\/ARITH.2009.28","DOI":"10.1109\/ARITH.2009.28"}],"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-032-32519-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:23Z","timestamp":1784791043000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}