{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:17Z","timestamp":1784830877664,"version":"3.55.0"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P27722, W1255-N23"],"award-info":[{"award-number":["P27722, W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-103"],"award-info":[{"award-number":["ICT15-103"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states.<\/jats:p>\n          <jats:p>In this paper, we present APALACHE -- a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, APALACHE translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers. Designing this translation is the central challenge that we address in this paper. Our experiments show that APALACHE outperforms TLC on examples with large state spaces.<\/jats:p>","DOI":"10.1145\/3360549","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["TLA+ model checking made symbolic"],"prefix":"10.1145","volume":"3","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[{"name":"Inria, France \/ LORIA, France \/ University of Lorraine, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jure","family":"Kukovec","sequence":"additional","affiliation":[{"name":"TU Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thanh-Hai","family":"Tran","sequence":"additional","affiliation":[{"name":"TU Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/MoDRE.2018.00008"},{"key":"e_1_2_1_2_1","volume-title":"The B-book: assigning programs to meanings","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial . 2005. The B-book: assigning programs to meanings . Cambridge University Press . Jean-Raymond Abrial. 2005. The B-book: assigning programs to meanings. Cambridge University Press."},{"key":"e_1_2_1_3_1","volume-title":"6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z","author":"ABZ.","year":"2018","unstructured":"ABZ. 2018 . 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z , 2018. ABZ. 2018. 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 2018."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/983102"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.08.003"},{"key":"e_1_2_1_6_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2001","unstructured":"Thomas Ball , Rupak Majumdar , Todd D. Millstein , and Sriram K . Rajamani . 2001 . Automatic Predicate Abstraction of C Programs. In PLDI. 203\u2013213. Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In PLDI. 203\u2013213."},{"key":"e_1_2_1_7_1","volume-title":"International Symposium on Formal Methods for Components and Objects. Springer, 364\u2013387","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett , Bor-Yuh Evan Chang , Robert DeLine , Bart Jacobs , and K Rustan M Leino . 2005 . Boogie: A modular reusable verifier for object-oriented programs . In International Symposium on Formal Methods for Components and Objects. Springer, 364\u2013387 . Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K Rustan M Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In International Symposium on Formal Methods for Components and Objects. Springer, 364\u2013387."},{"key":"e_1_2_1_8_1","volume-title":"International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices . Springer, 49\u201369","author":"Barnett Mike","year":"2004","unstructured":"Mike Barnett , K Rustan M Leino , and Wolfram Schulte . 2004 . The Spec# programming system: An overview . In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices . Springer, 49\u201369 . Mike Barnett, K Rustan M Leino, and Wolfram Schulte. 2004. The Spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices . Springer, 49\u201369."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_22"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Idan Berkovits Marijana Lazic Giuliano Losa Oded Padon and Sharon Shoham. 2019. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In CAV. 245\u2013266.  Idan Berkovits Marijana Lazic Giuliano Losa Oded Padon and Sharon Shoham. 2019. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In CAV. 245\u2013266.","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_2_1_12_1","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions . Springer Science & amp; Business Media. Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions . Springer Science &amp; Business Media."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"e_1_2_1_14_1","volume-title":"SICStus Prolog user\u2019s manual","author":"Carlsson Mats","unstructured":"Mats Carlsson , Johan Widen , Johan Andersson , Stefan Andersson , Kent Boortz , Hans Nilsson , and Thomas Sj\u00f6land . 1988. SICStus Prolog user\u2019s manual . Vol. 3 . Swedish Institute of Computer Science Kista , Sweden . Mats Carlsson, Johan Widen, Johan Andersson, Stefan Andersson, Kent Boortz, Hans Nilsson, and Thomas Sj\u00f6land. 1988. SICStus Prolog user\u2019s manual . Vol. 3. Swedish Institute of Computer Science Kista, Sweden."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"e_1_2_1_17_1","volume-title":"Theoretical aspects of computing","author":"Chaudhuri Kaustuv","unstructured":"Kaustuv Chaudhuri , Damien Doligez , Leslie Lamport , and Stephan Merz . 2010. The TLA + proof system: Building a heterogeneous verification platform . In Theoretical aspects of computing . Springer-Verlag , 44\u201344. Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. 2010. The TLA + proof system: Building a heterogeneous verification platform. In Theoretical aspects of computing. Springer-Verlag, 44\u201344."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In CONCUR (LNCS). 317\u2013331.  Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In CONCUR (LNCS). 317\u2013331.","DOI":"10.1007\/BFb0055631"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Maximiliano Cristi\u00e1 and Gianfranco Rossi. 2016. A Decision Procedure for Sets Binary Relations and Partial Functions. In CAV . 179\u2013198.  Maximiliano Cristi\u00e1 and Gianfranco Rossi. 2016. A Decision Procedure for Sets Binary Relations and Partial Functions. In CAV . 179\u2013198.","DOI":"10.1007\/978-3-319-41528-4_10"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Andrei Damian Cezara Dragoi Alexandru Militaru and Josef Widder. 2019. Communication-Closed Asynchronous Protocols. In CAV. 344\u2013363.  Andrei Damian Cezara Dragoi Alexandru Militaru and Josef Widder. 2019. Communication-Closed Asynchronous Protocols. In CAV. 344\u2013363.","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"e_1_2_1_24_1","first-page":"337","article-title":"Z3: An efficient SMT solver","volume":"1579","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008 . Z3: An efficient SMT solver . In TACAS. LNCS , Vol. 1579. 337 \u2013 340 . Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS. LNCS, Vol. 1579. 337\u2013340.","journal-title":"TACAS. LNCS"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.161.13"},{"key":"e_1_2_1_26_1","first-page":"161","article-title":"A Logic-based Framework for Verifying Consensus Algorithms","volume":"8318","author":"Dr\u0103goi Cezara","year":"2014","unstructured":"Cezara Dr\u0103goi , Thomas A. Henzinger , Helmut Veith , Josef Widder , and Damien Zufferey . 2014 . A Logic-based Framework for Verifying Consensus Algorithms . In VMCAI (LNCS) , Vol. 8318. 161 \u2013 181 . Cezara Dr\u0103goi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. 2014. A Logic-based Framework for Verifying Consensus Algorithms. In VMCAI (LNCS), Vol. 8318. 161\u2013181.","journal-title":"VMCAI (LNCS)"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Cezara Dr\u0103goi Thomas A. Henzinger and Damien Zufferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In POPL. 400\u2013415.  Cezara Dr\u0103goi Thomas A. Henzinger and Damien Zufferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In POPL. 400\u2013415.","DOI":"10.1145\/2914770.2837650"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_12"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan Zachary Kincaid and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In LICS. 185\u2013196.  Azadeh Farzan Zachary Kincaid and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In LICS. 185\u2013196.","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-002-0070-8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755950"},{"key":"e_1_2_1_35_1","unstructured":"Jason Gustafson. 2019. Kafka Improvement Proposal 320. https:\/\/cwiki.apache.org\/confluence\/display\/KAFKA\/KIP-320%3A+Allow+fetchers+to+detect+and+handle+log+truncation  Jason Gustafson. 2019. Kafka Improvement Proposal 320. https:\/\/cwiki.apache.org\/confluence\/display\/KAFKA\/KIP-320%3A+Allow+fetchers+to+detect+and+handle+log+truncation"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Dominik Hansen and Michael Leuschel. 2012. Translating TLA + to B for Validation with ProB. In IFM. 24\u201338.  Dominik Hansen and Michael Leuschel. 2012. Translating TLA + to B for Validation with ProB. In IFM. 24\u201338.","DOI":"10.1007\/978-3-642-30729-4_3"},{"key":"e_1_2_1_37_1","first-page":"7","article-title":"IronFleet","volume":"60","author":"Hawblitzel Chris","year":"2017","unstructured":"Chris Hawblitzel , Jon Howell , Manos Kapritsos , Jacob R. Lorch , Bryan Parno , Michael L. Roberts , Srinath Setty , and Brian Zill . 2017 . IronFleet : Proving Safety and Liveness of Practical Distributed Systems. Commun. ACM 60 , 7 (June 2017), 83\u201392. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2017. IronFleet: Proving Safety and Liveness of Practical Distributed Systems. Commun. ACM 60, 7 (June 2017), 83\u201392.","journal-title":"Proving Safety and Liveness of Practical Distributed Systems. Commun. ACM"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_39_1","volume-title":"The SPIN Model Checker","author":"Holzmann Gerard","unstructured":"Gerard Holzmann . 2003. The SPIN Model Checker . Addison-Wesley . Gerard Holzmann. 2003. The SPIN Model Checker. Addison-Wesley."},{"key":"e_1_2_1_40_1","first-page":"1","article-title":"Flexible Paxos","volume":"25","author":"Howard Heidi","year":"2016","unstructured":"Heidi Howard , Dahlia Malkhi , and Alexander Spiegelman . 2016 . Flexible Paxos : Quorum Intersection Revisited. In OPODIS. 25 : 1 \u2013 25 :14. Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum Intersection Revisited. In OPODIS. 25:1\u201325:14.","journal-title":"Quorum Intersection Revisited. In OPODIS."},{"key":"e_1_2_1_41_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson Daniel","unstructured":"Daniel Jackson . 2012. Software Abstractions: logic, language, and analysis . MIT press . Daniel Jackson. 2012. Software Abstractions: logic, language, and analysis. MIT press."},{"key":"e_1_2_1_42_1","volume-title":"Systematic software development using VDM","author":"Jones Cliff B","unstructured":"Cliff B Jones . 1990. Systematic software development using VDM . Vol. 2 . Prentice Hall Englewood Cliffs . Cliff B Jones. 1990. Systematic software development using VDM. Vol. 2. Prentice Hall Englewood Cliffs."},{"key":"e_1_2_1_43_1","unstructured":"Igor Konnov Jure Kukovec and Thanh-Hai Tran. 2019. APALACHE Model Checker. https:\/\/github.com\/konnov\/apalache .  Igor Konnov Jure Kukovec and Thanh-Hai Tran. 2019. APALACHE Model Checker. https:\/\/github.com\/konnov\/apalache ."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0297-4"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Igor Konnov Marijana Lazi\u0107 Helmut Veith and Josef Widder. 2017b. A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms. In POPL. 719\u2013734.  Igor Konnov Marijana Lazi\u0107 Helmut Veith and Josef Widder. 2017b. A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms. In POPL. 719\u2013734.","DOI":"10.1145\/3093333.3009860"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_6"},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Jure Kukovec Thanh-Hai Tran and Igor Konnov. 2018. Extracting Symbolic Transitions from TLA+ Specifications. In Abstract State Machines Alloy B TLA VDM and Z . 89\u2013104.  Jure Kukovec Thanh-Hai Tran and Igor Konnov. 2018. Extracting Symbolic Transitions from TLA+ Specifications. In Abstract State Machines Alloy B TLA VDM and Z . 89\u2013104.","DOI":"10.1007\/978-3-319-91271-4_7"},{"key":"e_1_2_1_48_1","volume-title":"Huu Hai Nguyen, and Martin C. Rinard","author":"Kuncak Viktor","year":"2005","unstructured":"Viktor Kuncak , Huu Hai Nguyen, and Martin C. Rinard . 2005 . An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. In CADE. 260\u2013277. Viktor Kuncak, Huu Hai Nguyen, and Martin C. Rinard. 2005. An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. In CADE. 260\u2013277."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_50_1","volume-title":"Specifying systems: The TLA+ language and tools for hardware and software engineers","author":"Lamport Leslie","unstructured":"Leslie Lamport . 2002. Specifying systems: The TLA+ language and tools for hardware and software engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley."},{"key":"e_1_2_1_51_1","volume-title":"DISC (LNCS)","author":"Lamport Leslie","unstructured":"Leslie Lamport . 2011. Byzantizing Paxos by Refinement . In DISC (LNCS) , Vol. 6950 . Springer , 211\u2013224. Leslie Lamport. 2011. Byzantizing Paxos by Refinement. In DISC (LNCS), Vol. 6950. Springer, 211\u2013224."},{"key":"e_1_2_1_52_1","unstructured":"Leslie Lamport. 2018. TLA +2 : A Preliminary Guide. https:\/\/lamport.azurewebsites.net\/tla\/tla2-guide.pdf  Leslie Lamport. 2018. TLA +2 : A Preliminary Guide. https:\/\/lamport.azurewebsites.net\/tla\/tla2-guide.pdf"},{"key":"e_1_2_1_53_1","first-page":"18","article-title":"Paxos made simple","volume":"32","author":"Leslie Lamport","year":"2001","unstructured":"Leslie Lamport et al. 2001 . Paxos made simple . ACM Sigact News 32 , 4 (2001), 18 \u2013 25 . Leslie Lamport et al. 2001. Paxos made simple. ACM Sigact News 32, 4 (2001), 18\u201325.","journal-title":"ACM Sigact News"},{"key":"e_1_2_1_54_1","unstructured":"Butler Lampson and Howard E Sturgis. 1979. Crash recovery in a distributed data storage system. (1979).  Butler Lampson and Howard E Sturgis. 1979. Crash recovery in a distributed data storage system. (1979)."},{"key":"e_1_2_1_55_1","volume-title":"This is boogie 2. manuscript KRML 178, 131","author":"Leino K Rustan M","year":"2008","unstructured":"K Rustan M Leino . 2008. This is boogie 2. manuscript KRML 178, 131 ( 2008 ), 9. K Rustan M Leino. 2008. This is boogie 2. manuscript KRML 178, 131 (2008), 9."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220900.3221117"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_59_1","unstructured":"Nancy A Lynch. 1996. Distributed algorithms. Morgan Kaufmann.  Nancy A Lynch. 1996. Distributed algorithms. Morgan Kaufmann."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90066-7"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950318"},{"key":"e_1_2_1_62_1","volume-title":"Alloy meets TLA+: An exploratory study. arXiv preprint arXiv:1603.03599","author":"Macedo Nuno","year":"2016","unstructured":"Nuno Macedo and Alcino Cunha . 2016. Alloy meets TLA+: An exploratory study. arXiv preprint arXiv:1603.03599 ( 2016 ). Nuno Macedo and Alcino Cunha. 2016. Alloy meets TLA+: An exploratory study. arXiv preprint arXiv:1603.03599 (2016)."},{"key":"e_1_2_1_63_1","volume-title":"Basin","author":"Maric Ognjen","year":"2017","unstructured":"Ognjen Maric , Christoph Sprenger , and David A . Basin . 2017 . Cutoff Bounds for Consensus Algorithms. In CAV. 217\u2013237. Ognjen Maric, Christoph Sprenger, and David A. Basin. 2017. Cutoff Bounds for Consensus Algorithms. In CAV. 217\u2013237."},{"key":"e_1_2_1_64_1","volume-title":"Symbolic Model Checking","author":"McMillan Kenneth L","unstructured":"Kenneth L McMillan . 1993. The SMV system . In Symbolic Model Checking . Springer , 61\u201385. Kenneth L McMillan. 1993. The SMV system. In Symbolic Model Checking. Springer, 61\u201385."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_10"},{"key":"e_1_2_1_67_1","volume-title":"Logics of Specification Languages, Dines Bj\u00f8rner and Martin C","author":"Merz Stephan","unstructured":"Stephan Merz . 2008. The Specification Language TLA + . In Logics of Specification Languages, Dines Bj\u00f8rner and Martin C . Henson (Eds.). Springer , Berlin- Heidelberg , 401\u2013451. Stephan Merz. 2008. The Specification Language TLA + . In Logics of Specification Languages, Dines Bj\u00f8rner and Martin C. Henson (Eds.). Springer, Berlin-Heidelberg, 401\u2013451."},{"key":"e_1_2_1_68_1","first-page":"3","article-title":"On the Logic of TLA +","volume":"22","author":"Merz Stephan","year":"2012","unstructured":"Stephan Merz . 2012 . On the Logic of TLA + . Computing and Informatics 22 , 3 - 4 (2012), 351\u2013379. Stephan Merz. 2012. On the Logic of TLA + . Computing and Informatics 22, 3-4 (2012), 351\u2013379.","journal-title":"Computing and Informatics"},{"key":"e_1_2_1_69_1","volume-title":"LPAR","author":"Merz Stephan","unstructured":"Stephan Merz and Hern\u00e1n Vanzetto . 2012. Automatic Verification of TLA + Proof Obligations with SMT Solvers .. In LPAR , Vol. 7180 . Springer , 289\u2013303. Stephan Merz and Hern\u00e1n Vanzetto. 2012. Automatic Verification of TLA + Proof Obligations with SMT Solvers.. In LPAR, Vol. 7180. Springer, 289\u2013303."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.09.004"},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Iulian Moraru David G Andersen and Michael Kaminsky. 2013. There is more consensus in egalitarian parliaments. In SOSP . ACM 358\u2013372.  Iulian Moraru David G Andersen and Michael Kaminsky. 2013. There is more consensus in egalitarian parliaments. In SOSP . ACM 358\u2013372.","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_74_1","volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic . Vol. 2283 . Springer Science & amp; Business Media. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science &amp; Business Media."},{"key":"e_1_2_1_75_1","unstructured":"Diego Ongaro. 2014. Consensus: Bridging theory and practice. Ph.D. Dissertation. Stanford University.  Diego Ongaro. 2014. Consensus: Bridging theory and practice. Ph.D. Dissertation. Stanford University."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_31"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.009"},{"key":"e_1_2_1_80_1","volume-title":"Communication and Agreement Abstractions for Fault-Tolerant Asynchronous Distributed Systems. Morgan &amp","author":"Raynal Michel","unstructured":"Michel Raynal . 2010. Communication and Agreement Abstractions for Fault-Tolerant Asynchronous Distributed Systems. Morgan &amp ; Claypool Publishers . Michel Raynal. 2010. Communication and Agreement Abstractions for Fault-Tolerant Asynchronous Distributed Systems. Morgan &amp; Claypool Publishers."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_1_82_1","volume-title":"The Z notation","author":"Michael Spivey J","unstructured":"J Michael Spivey and JR Abrial . 1992. The Z notation . Prentice Hall Hemel Hempstead . J Michael Spivey and JR Abrial. 1992. The Z notation. Prentice Hall Hemel Hempstead."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_84_1","volume-title":"Reasoning with Finite Sets and Cardinality Constraints in SMT. Logical Methods in Computer Science 14","author":"Tinelli Cesare","year":"2018","unstructured":"Cesare Tinelli , Andrew Reynolds , Clark Barrett , and Kshitij Bansal . 2018. Reasoning with Finite Sets and Cardinality Constraints in SMT. Logical Methods in Computer Science 14 ( 2018 ). Cesare Tinelli, Andrew Reynolds, Clark Barrett, and Kshitij Bansal. 2018. Reasoning with Finite Sets and Cardinality Constraints in SMT. Logical Methods in Computer Science 14 (2018)."},{"key":"e_1_2_1_85_1","unstructured":"TLAPlus. 2019. A collection of TLA+ specifications of varying complexities. https:\/\/github.com\/tlaplus\/Examples  TLAPlus. 2019. A collection of TLA+ specifications of varying complexities. https:\/\/github.com\/tlaplus\/Examples"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"e_1_2_1_87_1","doi-asserted-by":"crossref","unstructured":"Klaus von Gleissenthall Nikolaj Bj\u00f8rner and Andrey Rybalchenko. 2016. Cardinalities and universal quantifiers for verifying parameterized systems. In PLDI. 599\u2013613.  Klaus von Gleissenthall Nikolaj Bj\u00f8rner and Andrey Rybalchenko. 2016. Cardinalities and universal quantifiers for verifying parameterized systems. In PLDI. 599\u2013613.","DOI":"10.1145\/2980983.2908129"},{"key":"e_1_2_1_88_1","volume-title":"Alexander Bakst, Deian Stefan, and Ranjit Jhala.","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall , Rami G\u00f6khan Kici , Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019 . Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3, POPL ( 2019), 59:1\u201359:30. Klaus von Gleissenthall, Rami G\u00f6khan Kici, Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019. Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3, POPL (2019), 59:1\u201359:30."},{"key":"e_1_2_1_89_1","doi-asserted-by":"crossref","unstructured":"Hillel Wayne. 2018. Practical TLA+. Apress.  Hillel Wayne. 2018. Practical TLA+. Apress.","DOI":"10.1007\/978-1-4842-3829-5"},{"key":"e_1_2_1_90_1","volume-title":"Anderson","author":"Wilcox James R.","year":"2015","unstructured":"James R. Wilcox , Doug Woos , Pavel Panchekha , Zachary Tatlock , Xi Wang , Michael D. Ernst , and Thomas E . Anderson . 2015 . Verdi: a framework for implementing and formally verifying distributed systems. In PLDI. 357\u2013368. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In PLDI. 357\u2013368."},{"key":"e_1_2_1_91_1","doi-asserted-by":"crossref","unstructured":"Kuat Yessenov Ruzica Piskac and Viktor Kuncak. 2010. Collections Cardinalities and Relations. In VMCAI. 380\u2013395.  Kuat Yessenov Ruzica Piskac and Viktor Kuncak. 2010. Collections Cardinalities and Relations. In VMCAI. 380\u2013395.","DOI":"10.1007\/978-3-642-11319-2_27"},{"key":"e_1_2_1_92_1","volume-title":"Correct Hardware Design and Verification Methods","author":"Yu Yuan","unstructured":"Yuan Yu , Panagiotis Manolios , and Leslie Lamport . 1999. Model checking TLA + specifications . In Correct Hardware Design and Verification Methods . Springer , 54\u201366. Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model checking TLA + specifications. In Correct Hardware Design and Verification Methods . Springer, 54\u201366."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0302-2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360549","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360549","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360549"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":92,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360549"],"URL":"https:\/\/doi.org\/10.1145\/3360549","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}