{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:54:31Z","timestamp":1783018471599,"version":"3.54.6"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"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                    SMT solving with ordering consistency theory achieves state-of-the-art efficiency\u00a0in bounded model checking of concurrent programs. At its core is a dedicated theory solver that derives the write-serialization (WS) and from-read (FR) orders on the fly, thereby allowing their explicit encodings to be omitted. Additionally, the solver is equipped with\n                    <jats:italic>preventive propagation<\/jats:italic>\n                    , which proactively eliminates theory-level conflicts. This work presents a refined ordering consistency theory that overcomes two existing limitations. First, we address the\n                    <jats:italic>weak SC problem<\/jats:italic>\n                    , where the solver may fail to reconstruct a total WS order\u00a0and thus admit executions weaker than Sequential Consistency. We identify the core reason as insufficient constraints on WS totality. As a solution, we restore the WS encodings to ensure its totality, while preserving WS derivation to curb the resulting growth in the search space. Second, the existing framework for preventive propagation does\u00a0not support WS variables or atomicity constraints. We extend it to incorporate these elements, yielding a more general and principled propagation mechanism. Experiments show that our approach soundly prevents weak-SC behaviors, enables effective propagation, and maintains competitive overall performance.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_26","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:22Z","timestamp":1779033022000},"page":"500-519","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Refined Ordering Consistency Theory: Full Sequential Consistency and\u00a0Generalized Preventive Reasoning"],"prefix":"10.1007","author":[{"given":"Zhiheng","family":"Cai","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhihang","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201914, New York, NY, USA, pp. 373\u2013384. Association for Computing Machinery (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2535838.2535845"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"26_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ng, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360576","DOI":"10.1145\/3360576"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 258\u2013272. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_25"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-90643-5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Bajczi","year":"2025","unstructured":"Bajczi, L., Telbisz, C., Szekeres, D., V\u00f6r\u00f6s, A.: On stability in a happens-before propagator for concurrent programs (reproducibility study). In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025. LNCS, vol. 15696, pp. 3\u201319. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_1"},{"key":"26_CR7","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-030-99527-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: TACAS 2022, Part II. LNCS, vol. 13244, pp. 375\u2013402. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part II. LNCS, vol. 13994, pp. 495\u2013522. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"26_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025, Part III. LNCS, vol. 15698, pp. 151\u2013186. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"26_CR11","doi-asserted-by":"publisher","unstructured":"Biswas, R., Enea, C.: On the complexity of checking transactional consistency. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360591","DOI":"10.1145\/3360591"},{"key":"26_CR12","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Eisenhofer, C., Kov\u00e1cs, L.: Satisfiability modulo custom theories in Z3. In: Dragoi, C., Emmi, M., Wang, J. (eds.) VMCAI 2023. LNCS, vol. 13881, pp. 91\u2013105. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_5","DOI":"10.1007\/978-3-031-24950-1_5"},{"key":"26_CR13","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Rom\u00e1n-Calvo, E.: On the complexity of checking mixed isolation levels for SQL transactions. In: Piskac and Z. Rakamari\u0107 (Eds.) CAV 2025, Part IV. LNCS, vol. 15934, pp. 315\u2013337. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_15","DOI":"10.1007\/978-3-031-98685-7_15"},{"key":"26_CR14","doi-asserted-by":"publisher","unstructured":"Cai, Z., Sun, Z., He, F.: Artifact for \u201ca refined ordering consistency theory: full sequential consistency and generalized preventive reasoning\u201d (2026). https:\/\/doi.org\/10.5281\/zenodo.18616443","DOI":"10.5281\/zenodo.18616443"},{"issue":"1","key":"26_CR15","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Form. Methods Syst. Des."},{"issue":"7","key":"26_CR16","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun. ACM"},{"issue":"9","key":"26_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011). https:\/\/doi.org\/10.1145\/1995376.1995394","journal-title":"Commun. ACM"},{"key":"26_CR18","doi-asserted-by":"publisher","unstructured":"Fan, H., Sun, Z., He, F.: Satisfiability modulo ordering consistency theory for SC, TSO, and PSO memory models. ACM Trans. Program. Lang. Syst. 45(1) (2023). https:\/\/doi.org\/10.1145\/3579835","DOI":"10.1145\/3579835"},{"key":"26_CR19","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201905, New York, NY, USA, pp. 110\u2013121. Association for Computing Machinery (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"26_CR20","doi-asserted-by":"publisher","unstructured":"Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory-model-aware testing: a unified complexity analysis. ACM Trans. Embed. Comput. Syst. 14(4) (2015). https:\/\/doi.org\/10.1145\/2753761","DOI":"10.1145\/2753761"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-85114-1_10","volume-title":"Model Checking Software","author":"MK Ganai","year":"2008","unstructured":"Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 114\u2013133. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85114-1_10"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-25540-4_19","volume-title":"Computer Aided Verification","author":"N Gavrilenko","year":"2019","unstructured":"Gavrilenko, N., Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 355\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19"},{"issue":"4","key":"26_CR23","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997). https:\/\/doi.org\/10.1137\/S0097539794279614","journal-title":"SIAM J. Comput."},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"Haas, T., Meyer, R., Ponce\u00a0de Le\u00f3n, H.: CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563292","DOI":"10.1145\/3563292"},{"key":"26_CR25","doi-asserted-by":"publisher","unstructured":"He, F., Sun, Z., Fan, H.: Satisfiability modulo ordering consistency theory for multi-threaded program verification. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021, New York, NY, USA, pp. 1264\u20131279. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454108","DOI":"10.1145\/3453483.3454108"},{"key":"26_CR26","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498711","DOI":"10.1145\/3498711"},{"key":"26_CR27","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Vafeiadis, V.: Spore: combining symmetry and partial order reduction. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656449","DOI":"10.1145\/3656449"},{"key":"26_CR28","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2019, New York, NY, USA, pp. 96\u2013110. Association for Computing Machinery (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","DOI":"10.1145\/3314221.3314609"},{"key":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"issue":"9","key":"26_CR30","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans. Comput."},{"issue":"6","key":"26_CR31","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract davis-putnam-logemann-loveland procedure to dpll(t). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"issue":"2","key":"26_CR32","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988). https:\/\/doi.org\/10.1145\/42190.42277","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR33","doi-asserted-by":"publisher","unstructured":"Sun, Z., Fan, H., He, F.: Consistency-preserving propagation for SMT solving of concurrent program verification. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563321","DOI":"10.1145\/3563321"},{"key":"26_CR34","doi-asserted-by":"publisher","unstructured":"Telbisz, C., Bajczi, L., Szekeres, D., V\u00f6r\u00f6s, A.: Theta: Various approaches for concurrent program verification (competition contribution). In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025, Part III. LNCS, vol. 15698, pp. 260\u2013265. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_22","DOI":"10.1007\/978-3-031-90660-2_22"},{"key":"26_CR35","doi-asserted-by":"publisher","unstructured":"T\u00f3th, T., Hajdu, A., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: Stewart, D., Weissenbacher, G. (eds.) Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, pp. 176\u2013179 (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102257","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"26_CR36","doi-asserted-by":"publisher","unstructured":"Wang, C., Jin, H., Hachtel, G.D., Somenzi, F.: Refining the sat decision ordering for bounded model checking. In: Proceedings of the 41st Annual Design Automation Conference. DAC \u201904, New York, NY, USA, pp. 535\u2013538. Association for Computing Machinery (2004). https:\/\/doi.org\/10.1145\/996566.996713","DOI":"10.1145\/996566.996713"},{"issue":"6","key":"26_CR37","doi-asserted-by":"publisher","first-page":"781","DOI":"10.1007\/s00165-011-0179-2","volume":"23","author":"C Wang","year":"2011","unstructured":"Wang, C., Kundu, S., Limaye, R., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. Form. Asp. Comput. 23(6), 781\u2013805 (2011). https:\/\/doi.org\/10.1007\/s00165-011-0179-2","journal-title":"Form. Asp. Comput."},{"key":"26_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-89963-3_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Yin","year":"2018","unstructured":"Yin, L., Dong, W., Liu, W., Li, Y., Wang, J.: YOGAR-CBMC: CBMC with scheduling constraint based abstraction refinement. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 422\u2013426. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_25"},{"key":"26_CR39","doi-asserted-by":"publisher","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Scheduling constraint based abstraction refinement for weak memory models. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering.ASE \u201918, New York, NY, USA, pp. 645\u2013655. Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3238147.3238223","DOI":"10.1145\/3238147.3238223"},{"key":"26_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-030-59152-6_20","volume-title":"Automated Technology for Verification and Analysis","author":"R Zennou","year":"2020","unstructured":"Zennou, R., Atig, M.F., Biswas, R., Bouajjani, A., Enea, C., Erradi, M.: Boosting sequential consistency checking using saturation. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 360\u2013376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_20"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:47:31Z","timestamp":1783014451000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_26","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The artifact for this paper is available on Zenodo\u00a0[\n                      \n                      ].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}