{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:34:20Z","timestamp":1771472060530,"version":"3.50.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The need to provide formal guarantees about the behaviour of the algorithms underpinning modern distributed systems became evident in recent years. This interest made apparent the complexities involved in applying verification techniques in a distributed setting, with significant effort being made in both academia and industry to aid in this endeavour. Many formalisms have been proposed to tackle the difficulties faced by practitioners, with one that has seen widespread use in industry being TLA<jats:inline-formula><jats:alternatives><jats:tex-math>$$^+$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow\/><mml:mo>+<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, adopted, for instance, by Amazon Web Services. TLA<jats:inline-formula><jats:alternatives><jats:tex-math>$$^+$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow\/><mml:mo>+<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>provides engineers with a way of specifying both systems and desired properties, and is supported by a number of verification tools. Despite their extensive use, such tools suffer considerably from lack of scalability. To solve this, we propose a novel encoding of TLA<jats:inline-formula><jats:alternatives><jats:tex-math>$$^+$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow\/><mml:mo>+<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>into SMT constraints to improve symbolic model checking efficiency. Our insight is the need to provide the SMT solver with structural information about the TLA<jats:inline-formula><jats:alternatives><jats:tex-math>$$^+$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow\/><mml:mo>+<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>specification encoded, i.e., how data structures and their component elements interact, which we do by relying on the SMT theory of arrays. We implemented our approach by modifying the SMT-based model checker<jats:sc>Apalache<\/jats:sc>and evaluated it against comparable tools. Our results show that our approach outperforms existing ones on a number of benchmarks, with an order of magnitude improvement in checking time.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_7","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"126-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Model Checking for TLA+ Made Faster"],"prefix":"10.1007","author":[{"given":"Rodrigo","family":"Otoni","sequence":"first","affiliation":[]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[]},{"given":"Jure","family":"Kukovec","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Eugster","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. In: Proceedings of the 8th International Joint Conference on Automated Reasoning. pp. 82\u201398 (2016)","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: CVC5: A Versatile and Industrial-Strength SMT Solver. In: Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"7_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep. (2021), Available at https:\/\/smtlib.cs.uiowa.edu"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In: Proceedings of the 31st International Conference on Computer Aided Verification. pp. 245\u2013266 (2019)","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bracha, G., Toueg, S.: Asynchronous Consensus and Broadcast Protocols. Journal of the ACM 32(4), 824\u2013840 (1985)","DOI":"10.1145\/4221.214134"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA+ Proof System: Building a Heterogeneous Verification Platform. In: Proceedings of the 7th International Colloquium on the Theoretical Aspects of Computing. p.\u00a044 (2010)","DOI":"10.1007\/978-3-642-14808-8_3"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Generalized, Efficient Array Decision Procedures. In: Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design. pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Dobre, D., Suri, N.: One-step Consensus with Zero-Degradation. In: Proceedings of the 36th International Conference on Dependable Systems and Networks. pp. 137\u2013146 (2006)","DOI":"10.1109\/DSN.2006.55"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. In: Proceedings of the 13th NASA Formal Methods International Symposium. p. 131\u2013150 (2021)","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"7_CR11","unstructured":"Goel, A., Sakallah, K.A.: Towards an Automatic Proof of Lamport\u2019s Paxos. In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design. pp. 112\u2013122 (2021)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Guerraoui, R.: On the Hardness of Failure-Sensitive Agreement Problems. Information Processing Letters 79(2), 99\u2013104 (2001)","DOI":"10.1016\/S0020-0190(00)00171-X"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ Model Checking Made Symbolic. Proc. ACM Program. Lang. 3(OOPSLA), 123:1\u2013123:30 (2019)","DOI":"10.1145\/3360549"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kuppe, M., Merz, S.: Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. In: Proceedings of the 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. pp. 88\u2013105 (2022)","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Konnov, I., Lazi\u0107, M., Stoilkovska, I., Widder, J.: Tutorial: Parameterized Verification with Byzantine Model Checker. In: Proceedings of the 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems. pp. 189\u2013207 (2020)","DOI":"10.1007\/978-3-030-50086-3_11"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Kukovec, J., Tran, T.H., Konnov, I.: Extracting Symbolic Transitions from TLA+ Specifications. Science of Computer Programming 187, 102361 (2020)","DOI":"10.1016\/j.scico.2019.102361"},{"key":"7_CR17","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Merz, S., Vanzetto, H.: Encoding TLA+ into unsorted and many-sorted first-order logic. Science of Computer Programming 158, 3\u201320 (2018)","DOI":"10.1016\/j.scico.2017.09.004"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services uses Formal Methods. Communications of the ACM 58(4), 66\u201373 (2015)","DOI":"10.1145\/2699417"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety Verification by Interactive Generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 614\u2013630 (2016)","DOI":"10.1145\/2908080.2908118"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Schmidt, J., Leuschel, M.: Improving SMT Solver Integrations for the Validation of B and Event-B Models. In: Proceedings of the 26th International Conference on Formal Methods for Industrial Critical Systems. pp. 107\u2013125 (2021)","DOI":"10.1007\/978-3-030-85248-1_7"},{"key":"7_CR22","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design. pp. 273\u2013283 (2022)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Sivasubramanian, S.: Amazon DynamoDB: A Seamlessly Scalable Non-Relational Database Service. In: Proceedings of the 2012 ACM SIGMOD International Conference on Management of Data. p. 729\u2013730 (2012)","DOI":"10.1145\/2213836.2213945"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. International Journal on Software Tools for Technology Transfer 24(1), 33\u201348 (2022)","DOI":"10.1007\/s10009-021-00637-9"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C., Dill, D., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. pp. 29\u201337 (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"7_CR26","unstructured":"Tran, T.H.: Symbolic Verification of TLA+ Specifications with Applications to Distributed Algorithms. Ph.D. thesis, Technische Universit\u00e4t Wien (2023), upcoming thesis"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Proceedings of the 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. pp. 54\u201366 (1999)","DOI":"10.1007\/3-540-48153-2_6"}],"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-30823-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T00:17:21Z","timestamp":1729297041000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}