{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:16:51Z","timestamp":1771024611444,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031773815","type":"print"},{"value":"9783031773822","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_8","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:04Z","timestamp":1732562764000},"page":"126-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Validating Traces of\u00a0Distributed Programs Against TLA+ Specifications"],"prefix":"10.1007","author":[{"given":"Horatiu","family":"Cirstea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus A.","family":"Kuppe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Loillier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kuppe, M.A., Loillier, B., Merz, S.: Validating traces of distributed programs against TLA$$^{+}$$ specifications. arXiv:2404.16075 [cs.DC] (2024)","DOI":"10.1007\/978-3-031-77382-2_8"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA$$^{+}$$ Proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147\u2013154. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_14","DOI":"10.1007\/978-3-642-32759-9_14"},{"issue":"9","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1346","DOI":"10.14778\/3397230.3397233","volume":"13","author":"AJJ Davis","year":"2020","unstructured":"Davis, A.J.J., Hirschhorn, M., Schvimer, J.: eXtreme modelling in practice. Proc. VLDB Endowment 13(9), 1346\u20131358 (2020)","journal-title":"Proc. VLDB Endowment"},{"key":"8_CR4","unstructured":"Dijkstra, E.W.: EWD\u00a0998: Shmuel Safra\u2019s version of termination detection. http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd09xx\/EWD998.PDF (1987)"},{"key":"8_CR5","unstructured":"etcd project. TLA+ specification and trace validation for raft library: a brief guide. https:\/\/github.com\/etcd-io\/raft\/tree\/main\/tla (2024)"},{"key":"8_CR6","first-page":"141","volume":"34","author":"Y Falcone","year":"2013","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Depend. Softw. Syst. 34, 141\u2013175 (2013)","journal-title":"Eng. Depend. Softw. Syst."},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Fekete, A.: Snapshot Isolation. In: Liu, L., \u00d6zsu, M.T. (eds.) Encyclopedia of Database Systems, pp. 2659\u20132664. Springer US, Boston, MA (2009).https:\/\/doi.org\/10.1007\/978-0-387-39940-9_346","DOI":"10.1007\/978-0-387-39940-9_346"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Foo, D., Costea, A., Chin, W.-N.: Protocol conformance with\u00a0choreographic PlusCal. In: David, C., Sun, M. (eds.) Theoretical Aspects of Software Engineering: 17th International Symposium, TASE 2023, Bristol, UK, July 4\u20136, 2023, Proceedings, pp. 126\u2013145. Springer Nature Switzerland, Cham (2023).https:\/\/doi.org\/10.1007\/978-3-031-35257-7_8","DOI":"10.1007\/978-3-031-35257-7_8"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Hackett, F., Hosseini, S., Costa, R., Do, M., Beschastnikh, I.: Compiling distributed system models with PGo. In: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, vol. 2, pp. 159\u2013175, Vancouver BC Canada. ACM (2023)","DOI":"10.1145\/3575693.3575695"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K Havelund","year":"2000","unstructured":"Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245\u2013264. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_15"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"225","DOI":"10.14778\/3626292.3626304","volume":"17","author":"H Howard","year":"2023","unstructured":"Howard, H., et al.: Confidential Consortium Framework: secure multiparty applications with confidentiality, integrity, and high availability. Proc. VLDB Endowment 17(2), 225\u2013240 (2023)","journal-title":"Proc. VLDB Endowment"},{"key":"8_CR12","unstructured":"Howard, H., Kuppe, M.A., Ashton, E., Chamayou, A., Crooks, N.: Smart casual verification of CCF\u2019s distributed consensus and consistency protocols. arXiv:2406.17455 [cs.DC] (2024)"},{"key":"8_CR13","unstructured":"Howard, Y., Gruner, S., Gravell, A., Ferreira, C., Augusto, J.C.: Model-based trace-checking. arXiv:1111.2825 [cs] (2011)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.-H.: TLA+ model checking made symbolic. Proc. ACM Program. Lang., 3(OOPSLA) (2019)","DOI":"10.1145\/3360549"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kuppe, M., Merz, S.: Specification and\u00a0verification with\u00a0the\u00a0TLA+ Trifecta: TLC, Apalache, and\u00a0TLAPS. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles: 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22\u201330, 2022, Proceedings, Part I, pp. 88\u2013105. Springer International Publishing, Cham (2022).https:\/\/doi.org\/10.1007\/978-3-031-19849-6_6","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"8_CR16","unstructured":"Kuppe, M.A.: Implementing a TLA$$^{+}$$ specification: EWD998Chan. https:\/\/github.com\/tlaplus\/Examples\/pull\/75 (2023)"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Kuppe, M.A.: The TLA$$^{+}$$ debugger. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M., editors, Software Engineering and Formal Methods. SEFM 2022 Co-located Workshops, vol. 13765, pp. 174\u2013180. Springer, Cham (2023).https:\/\/doi.org\/10.1007\/978-3-031-26236-4_15","DOI":"10.1007\/978-3-031-26236-4_15"},{"key":"8_CR18","volume-title":"Specifying Systems","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Mass, Addison-Wesley, Boston (2002)"},{"key":"8_CR19","unstructured":"Lamport, L., et\u00a0al.: TLA$$^{+}$$ examples. https:\/\/github.com\/tlaplus\/examples\/"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","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 (2015)","journal-title":"Commun. ACM"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Niu, Z., Dong, L., Zhu, Y., Chen, L.: Verifying zookeeper based on model-based runtime trace-checking using TLA$$^{+}$$. In: Proceedings of the 7th International Conference on Cyber Security and Information Engineering, pp. 13\u201318, Brisbane QLD Australia. ACM (2022)","DOI":"10.1145\/3558819.3558822"},{"key":"8_CR22","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: 2014 USENIX Annual Technical Conference, pp. 305\u2013319, Philadelphia, PA (2014). USENIX Association"},{"key":"8_CR23","unstructured":"Pressler, R.: Conjunction capers: a TLA$$^{+}$$ truffle. https:\/\/conf.tlapl.us\/2020\/ (2020)"},{"key":"8_CR24","unstructured":"Schultz, W., Zhou, S., Dardik, I., Tripakis, S.: Design and analysis of a logless dynamic reconfiguration protocol. In: Bramas, Q., Gramoli, V., Milani, A., editors 25th International Conference Principles of Distributed Systems (OPODIS 2021), vol. 217 of LIPIcs, pp. 26:1-26:16, Strasbourg, France (2021). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"8_CR25","unstructured":"Tasiran, S., Yu, Y., Batson, B., Kreider, S.: Using formal specifications to monitor and guide simulation: verifying the cache coherence engine of the Alpha 21364 microprocessor. In: Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (2002)"},{"issue":"3","key":"8_CR26","first-page":"103","volume":"17","author":"J Tretmans","year":"1996","unstructured":"Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17(3), 103\u2013120 (1996)","journal-title":"Softw. Concepts Tools"},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/2967606","volume":"60","author":"FW Vaandrager","year":"2017","unstructured":"Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86\u201395 (2017)","journal-title":"Commun. ACM"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Wang, D., Dou, W., Gao, Y., Wu, C., Wei, J., Huang, T.: Model checking guided testing for distributed systems. In: Proceedings of the Eighteenth European Conference on Computer Systems, pp. 127\u2013143, Rome Italy. ACM (2023)","DOI":"10.1145\/3552326.3587442"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","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.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T23:53:34Z","timestamp":1733097214000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}