{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:18Z","timestamp":1779074478755,"version":"3.51.4"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:00:00Z","timestamp":1746230400000},"content-version":"vor","delay-in-days":122,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            <jats:sc>MoXI<\/jats:sc>\u00a0is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB\u00a02 language with constructs to define state-transition systems. The tool suite of <jats:sc>MoXI<\/jats:sc>\u00a0provides a translator from <jats:sc>MoXI<\/jats:sc>\u00a0to <jats:sc>Btor2<\/jats:sc>, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for <jats:sc>Btor2<\/jats:sc>\u00a0to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in <jats:sc>Btor2<\/jats:sc>. We present <jats:sc>MoXIchecker<\/jats:sc>, the first model checker that solves <jats:sc>MoXI<\/jats:sc>\u00a0verification tasks directly. Instead of translating <jats:sc>MoXI<\/jats:sc>\u00a0to lower-level languages, <jats:sc>MoXIchecker<\/jats:sc>\u00a0uses the solver-agnostic library <jats:sc>PySMT<\/jats:sc>\u00a0for SMT solvers as a backend for its verification algorithms. <jats:sc>MoXIchecker<\/jats:sc>\u00a0is <jats:italic>extensible<\/jats:italic> because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of <jats:sc>PySMT<\/jats:sc>. In our evaluation, <jats:sc>MoXIchecker<\/jats:sc>\u00a0uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the <jats:sc>MoXI<\/jats:sc>\u00a0tool suite.<\/jats:p>","DOI":"10.1007\/978-3-031-86695-1_1","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:54Z","timestamp":1746151614000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["MoXIchecker: An Extensible Model Checker for MoXI"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-2331-0955","authenticated-orcid":false,"given":"Salih","family":"Ates","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. In: Proc. LICS. pp. 428\u2013439. IEEE (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Symbolic Model Checking. Springer (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y., Dureja, R., Irfan, A., Johannsen, C., Nukala, K., Shankar, N., Tinelli, C., Vardi, M.Y.: MoXI: An intermediate language for symbolic model checking. In: Proc. SPIN. pp. 26\u201346. LNCS\u00a014624, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_2","DOI":"10.1007\/978-3-031-66149-5_2"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA\u00a0(1). pp. 143\u2013167. LNCS\u00a012476, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. J. Autom. Reasoning (2024). https:\/\/doi.org\/10.1007\/s10817-024-09702-9","DOI":"10.1007\/s10817-024-09702-9"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Jankola, M., Lee, N.Z.: A transferability study of interpolation-based hardware model checking for software verification. Proc. ACM Softw. Eng. 1(FSE) (2024). https:\/\/doi.org\/10.1145\/3660797","DOI":"10.1145\/3660797"},{"key":"1_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Tech. rep., University of Iowa (2010), https:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.0-r10.12.21.pdf"},{"key":"1_CR8","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: The VMT-LIB language and tools. In: Proc. SMT. CEUR Workshop Proceedings, vol.\u00a03185, pp. 80\u201389. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3185\/extended9547.pdf"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: The SMV system. In: Symbolic Model Checking, pp. 61\u201385 (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6_4","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"1_CR10","unstructured":"DeLine, R., Leino, R.: BoogiePL: A typed procedural language for checking object-oriented programs. Tech. Rep. MSR-TR-2005-70, Microsoft Research (2005). https:\/\/www.microsoft.com\/en-us\/research\/publication\/boogiepl-a-typed-procedural-language-for-checking-object-oriented-programs\/"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N.Z.: The transformation game: Joining forces for verification. In: Principles of Verification: Cycling the Probabilistic Landscape. pp. 175\u2013205. LNCS\u00a015262, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_9","DOI":"10.1007\/978-3-031-75778-5_9"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Johannsen, C., Nukala, K., Dureja, R., Irfan, A., Shankar, N., Tinelli, C., Vardi, M.Y., Rozier, K.Y.: The MoXI model exchange tool suite. In: Proc. CAV. pp. 203\u2013218. LNCS\u00a014681, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_10","DOI":"10.1007\/978-3-031-65627-9_10"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC, and Boolector 3.0. In: Proc. CAV. pp. 587\u2013595. LNCS\u00a010981, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.: AVR: Abstractly verifying reachability. In: Proc. TACAS. pp. 413\u2013422. LNCS\u00a012078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., Barrett, C.W.: Pono: A flexible and extensible SMT-based model checker. In: Proc. CAV. pp. 461\u2013474. LNCS\u00a012760, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"IEEE standard for Verilog hardware description language (2006). https:\/\/doi.org\/10.1109\/IEEESTD.2006.99495","DOI":"10.1109\/IEEESTD.2006.99495"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Minhas, M., Hasan, O., Saghar, K.: Ver2Smv: A tool for automatic Verilog to SMV translation for verifying digital circuits. In: Proc. ICEET. pp.\u00a01\u20135 (2018). https:\/\/doi.org\/10.1109\/ICEET1.2018.8338617","DOI":"10.1109\/ICEET1.2018.8338617"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: A tool for word-level verification. In: Proc. DATE. pp. 1156\u20131159 (2016), https:\/\/ieeexplore.ieee.org\/document\/7459485","DOI":"10.3850\/9783981537079_0765"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Mukherjee, R., Tautschnig, M., Kroening, D.: v2c: A Verilog to C translator. In: Proc. TACAS. pp. 580\u2013586. LNCS\u00a09636, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_38","DOI":"10.1007\/978-3-662-49674-9_38"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator. In: Proc. TACAS\u00a0(2). pp. 152\u2013172. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12","DOI":"10.1007\/978-3-031-30820-8_12"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Btor2-Cert: A certifying hardware-verification framework using software analyzers. In: Proc. TACAS\u00a0(3). pp. 129\u2013149. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_7","DOI":"10.1007\/978-3-031-57256-2_7"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Tafese, J., Garcia-Contreras, I., Gurfinkel, A.: Btor2MLIR: A format and toolchain for hardware verification. In: Proc. FMCAD. pp. 55\u201363. TU Wien Academic Press (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_13","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_13"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Chien, P.C., Lee, N.Z.: CPV: A circuit-based program verifier (competition contribution). In: Proc. TACAS\u00a0(3). pp. 365\u2013370. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_22","DOI":"10.1007\/978-3-031-57256-2_22"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Griggio, A., Jon\u00e1\u0161, M.: Kratos2: An SMT-based model checker for imperative programs. In: Proc. CAV. pp. 423\u2013436. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_20","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"1_CR25","unstructured":"Gario, M., Micheli, A.: PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proc. SMT (2015)"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. pp. 193\u2013207. LNCS\u00a01579, Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proc. FMCAD, pp. 127\u2013144. LNCS\u00a01954, Springer (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI. pp. 70\u201387. LNCS\u00a06538, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"1_CR29","unstructured":"Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge (1996). https:\/\/www.worldcat.org\/isbn\/978-0-41512-600-7"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Handbook of Model Checking, pp. 27\u201373. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model-checking competition 2017. In: Proc. FMCAD. p.\u00a09. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102233","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"1_CR33","unstructured":"PyVMT: A Python library to interact with transition systems. https:\/\/github.com\/pyvmt\/pyvmt, accessed: 2024-10-08"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. 31(4), 57:1\u201357:69 (2022). https:\/\/doi.org\/10.1145\/3477579","DOI":"10.1145\/3477579"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.09.009","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: Proc. CAV. pp. 334\u2013342. LNCS\u00a08559, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Proc. TACAS. pp. 46\u201361. LNCS\u00a08413, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proc. TACAS. pp. 337\u2013340. LNCS\u00a04963, Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS. pp. 93\u2013107. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Proc. CAV. pp. 737\u2013744. LNCS\u00a08559, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J.\u00a0Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","DOI":"10.2307\/2963593"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp. 1\u201313. LNCS\u00a02725, Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD. pp.\u00a01\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Intertwined forward-backward reachability analysis using interpolants. In: Proc. TACAS. pp. 308\u2013323. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_22","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Ates, S., Beyer, D., Chien, P.C., Lee, N.Z.: MoXIchecker release 0.2. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.13895872","DOI":"10.5281\/zenodo.13895872"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:07:02Z","timestamp":1746151622000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}