{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T08:04:17Z","timestamp":1764403457588,"version":"3.46.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"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,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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                    We present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA\n                    <jats:sup>+<\/jats:sup>\n                    . Our method\u2019s chief novelty lies in a new search space reduction technique called interpretation reduction, which allows to not only eliminate incorrect candidate protocols before they are sent to the verifier, but also to avoid enumerating redundant candidates in the first place. Further performance improvements are achieved by an advanced technique for exact generalization of counterexamples. Experiments on a set of established benchmarks show that our tool is almost always faster than the state of the art, often by orders of magnitude, and was also able to synthesize an entire TLA\n                    <jats:sup>+<\/jats:sup>\n                    protocol \u201cfrom scratch\u201d in less than 3 minutes where the state of the art timed out after an hour. Our method is sound, complete, and guaranteed to terminate on unrealizable synthesis instances under common assumptions which hold in all our benchmarks.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_8","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T07:32:26Z","timestamp":1746171146000},"page":"155-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction"],"prefix":"10.1007","author":[{"given":"Derek","family":"Egolf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp.\u00a01\u20138. IEEE (2013), https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing Finite-state Protocols from Scenarios and Requirements. In: Haifa Verification Conference. LNCS, vol.\u00a08855. Springer (2014)","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017. Lecture Notes in Computer Science, vol. 10205, pp. 319\u2013336 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18, https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017. Lecture Notes in Computer Science, vol. 10205, pp. 319\u2013336 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18, https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Alur, R., Tripakis, S.: Automatic synthesis of distributed protocols. SIGACT News 48(1), 55\u201390 (2017). https:\/\/doi.org\/10.1145\/3061640.3061652, https:\/\/doi.org\/10.1145\/3061640.3061652","DOI":"10.1145\/3061640.3061652"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Bloem, R., Braud-Santoni, N., Jacobs, S.: Synthesis of self-stabilising and byzantine-resilient distributed systems. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV. Lecture Notes in Computer Science, vol.\u00a09779, pp. 157\u2013176. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_9, https:\/\/doi.org\/10.1007\/978-3-319-41528-4_9","DOI":"10.1007\/978-3-319-41528-4_9"},{"key":"8_CR7","unstructured":"Buchman, E.: Tendermint: Byzantine fault tolerance in the age of blockchains (2016), https:\/\/api.semanticscholar.org\/CorpusID:59082906"},{"key":"8_CR8","unstructured":"Buterin, V.: Ethereum white paper: A next generation smart contract & decentralized application platform (2013), https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dean, J., Epstein, M., Fikes, A., Frost, C., Furman, J.J., Ghemawat, S., Gubarev, A., Heiser, C., Hochschild, P., et\u00a0al.: Spanner: Google\u2019s globally distributed database. ACM Transactions on Computer Systems (TOCS) 31(3), 1\u201322 (2013)","DOI":"10.1145\/2491245"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"DeCandia, G., Hastorun, D., Jampani, M., Kakulapati, G., Lakshman, A., Pilchin, A., Sivasubramanian, S., Vosshall, P., Vogels, W.: Dynamo: Amazon\u2019s highly available key-value store. ACM SIGOPS operating systems review 41(6), 205\u2013220 (2007)","DOI":"10.1145\/1323293.1294281"},{"key":"8_CR11","unstructured":"Egolf, D.: scythe-fmcad2024. https:\/\/github.com\/egolf-cs\/scythe-fmcad2024"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Egolf, D., Schultz, W., Tripakis, S.: Efficient synthesis of symbolic distributed protocols by sketching. In: Narodytska, N., R\u00fcmmer, P. (eds.) Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2024. pp. 281\u2013291. TU Wien Academic Press (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_34, https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_34","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_34"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Egolf, D., Tripakis, S.: Synthesis of distributed protocols by enumeration modulo isomorphisms. In: ATVA 2023 - Part I. pp. 270\u2013291. Lecture Notes in Computer Science, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_13, https:\/\/doi.org\/10.1007\/978-3-031-45329-8_13","DOI":"10.1007\/978-3-031-45329-8_13"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Egolf, D., Tripakis, S.: Accelerating protocol synthesis and detecting unrealizability with interpretation reduction (2025), https:\/\/arxiv.org\/abs\/2501.14585","DOI":"10.1007\/978-3-031-90653-4_8"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Fedchin, A., Dean, T., Foster, J.S., Mercer, E., Rakamaric, Z., Reger, G., Rungta, N., Salkeld, R., Wagner, L., Waldrip, C.: A toolkit for automated testing of dafny. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13903, pp. 397\u2013413. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_24, https:\/\/doi.org\/10.1007\/978-3-031-33170-1_24","DOI":"10.1007\/978-3-031-33170-1_24"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5-6), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/S10009-012-0228-Z, https:\/\/doi.org\/10.1007\/s10009-012-0228-z","DOI":"10.1007\/S10009-012-0228-Z"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizability of distributed fault-tolerant systems. Log. Methods Comput. Sci. 11(3) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:12)2015, https:\/\/doi.org\/10.2168\/LMCS-11(3:12)2015","DOI":"10.2168\/LMCS-11(3:12)2015"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. In: NASA Formal Methods: 13th International Symposium, NFM 2021. p. 131\u2013150 (2021)","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Foundations and Trends in Programming Languages 4(1-2), 1\u2013119 (2017). https:\/\/doi.org\/10.1561\/2500000010","DOI":"10.1561\/2500000010"},{"key":"8_CR20","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding Invariants of Distributed Systems: It\u2019s a Small (Enough) World After All. In: 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). pp. 115\u2013131. USENIX Association (Apr 2021), https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Hu, Q., Breck, J., Cyphert, J., D\u2019Antoni, L., Reps, T.W.: Proving unrealizability for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV. Lecture Notes in Computer Science, vol. 11561, pp. 335\u2013352. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_18, https:\/\/doi.org\/10.1007\/978-3-030-25540-4_18","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Hu, Q., Cyphert, J., D\u2019Antoni, L., Reps, T.W.: Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020. pp. 1128\u20131142. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385979, https:\/\/doi.org\/10.1145\/3385412.3385979","DOI":"10.1145\/3385412.3385979"},{"key":"8_CR23","unstructured":"Hui, Y., Ripberger, D., Lu, X., Wang, Y.: Learning distributed protocols with zero knowledge. In: Machine Learning for Systems at NeurIPS 2023 (2023), https:\/\/openreview.net\/forum?id=u0Ncut8ru5"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Synthesis of distributed agreement-based systems with efficiently-decidable verification. In: TACAS 2023. Lecture Notes in Computer Science, vol. 13994, pp. 289\u2013308. Springer (2023), https:\/\/doi.org\/10.1007\/978-3-031-30820-8_19","DOI":"10.1007\/978-3-031-30820-8_19"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:12)2014, https:\/\/doi.org\/10.2168\/LMCS-10(1:12)2014","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Haifa Verification Conference. p. 117-132. HVC\u201909, Springer (2009)","DOI":"10.1007\/978-3-642-19237-1_13"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Kim, J., D\u2019Antoni, L., Reps, T.W.: Unrealizability logic. Proc. ACM Program. Lang. 7(POPL), 659\u2013688 (2023). https:\/\/doi.org\/10.1145\/3571216, https:\/\/doi.org\/10.1145\/3571216","DOI":"10.1145\/3571216"},{"key":"8_CR28","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (Jun 2002)"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Lazic, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: 21st International Conference on Principles of Distributed Systems, OPODIS. LIPIcs, vol.\u00a095, pp. 32:1\u201332:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPICS.OPODIS.2017.32, https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2017.32","DOI":"10.4230\/LIPICS.OPODIS.2017.32"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Mirzaie, N., Faghih, F., Jacobs, S., Bonakdarpour, B.: Parameterized synthesis of self-stabilizing protocols in symmetric networks. Acta Informatica 57(1-2), 271\u2013304 (2020). https:\/\/doi.org\/10.1007\/S00236-019-00361-7, https:\/\/doi.org\/10.1007\/s00236-019-00361-7","DOI":"10.1007\/S00236-019-00361-7"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Nagy, S., Kim, J., D\u2019Antoni, L., Reps, T.W.: Automating unrealizability logic: Hoare-style proof synthesis for infinite sets of programs. CoRR abs\/2401.13244 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.13244, https:\/\/doi.org\/10.48550\/arXiv.2401.13244","DOI":"10.48550\/ARXIV.2401.13244"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services Uses Formal Methods. Commun. ACM 58(4), 66\u201373 (Mar 2015). https:\/\/doi.org\/10.1145\/2699417, http:\/\/doi.acm.org\/10.1145\/2699417","DOI":"10.1145\/2699417"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 179-190. POPL \u201989, Association for Computing Machinery, New York, NY, USA (1989). https:\/\/doi.org\/10.1145\/75277.75293, https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of the 31th IEEE Symposium on Foundations of Computer Science. pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Tinelli, C., Barrett, C.: CVC4SY: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Proceedings of the 31st International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 11561, pp. 74\u201383. Springer (Jul 2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5, http:\/\/theory.stanford.edu\/~barrett\/pubs\/RBN+19.pdf","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"8_CR36","unstructured":"Schultz, W., Ashton, E., Howard, H., Tripakis, S.: Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing. arXiv eprint 2404.18048 (2024)"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA$$ ^{\\text{+}}$$. In: 22nd Formal Methods in Computer-Aided Design, FMCAD 2022. pp. 273\u2013283. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_34, https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_34","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_34"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Proceedings of the 7th Asian Symposium on Programming Languages and Systems. pp. 4\u201313. APLAS \u201909, Springer (2009)","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf. 15(5-6), 475\u2013495 (oct 2013). https:\/\/doi.org\/10.1007\/s10009-012-0249-7, https:\/\/doi.org\/10.1007\/s10009-012-0249-7","DOI":"10.1007\/s10009-012-0249-7"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Thistle, J.G.: Undecidability in decentralized supervision. Systems & Control Letters 54(5), 503\u2013509 (2005). https:\/\/doi.org\/10.1016\/j.sysconle.2004.10.002","DOI":"10.1016\/j.sysconle.2004.10.002"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Tripakis, S.: Undecidable Problems of Decentralized Observation and Control on Regular Languages. Information Processing Letters 90(1), 21\u201328 (Apr 2004). https:\/\/doi.org\/10.1016\/j.ipl.2004.01.004","DOI":"10.1016\/j.ipl.2004.01.004"},{"key":"8_CR42","doi-asserted-by":"publisher","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16-19, 2013. pp. 287\u2013296. ACM (2013). https:\/\/doi.org\/10.1145\/2491956.2462174, https:\/\/doi.org\/10.1145\/2491956.2462174","DOI":"10.1145\/2491956.2462174"},{"key":"8_CR43","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In: Aguilera, M.K., Weatherspoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022). pp. 485\u2013501. USENIX Association (2022), https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: Mostly automated verification of liveness properties for distributed protocols with ranking functions. Proceedings of the ACM on Programming Languages (POPL) 8, 1028\u20131059 (jan 2024). https:\/\/doi.org\/10.1145\/3632877, https:\/\/doi.org\/10.1145\/3632877","DOI":"10.1145\/3632877"},{"key":"8_CR45","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In: 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2021). pp. 405\u2013421. USENIX Association (Jul 2021), https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"},{"key":"8_CR46","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods. pp. 54\u201366. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:42Z","timestamp":1764401802000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}