{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T14:13:13Z","timestamp":1725977593373},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912707"},{"type":"electronic","value":"9783319912714"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-91271-4_7","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:32:55Z","timestamp":1525689175000},"page":"89-104","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications"],"prefix":"10.1007","author":[{"given":"Jure","family":"Kukovec","sequence":"first","affiliation":[]},{"given":"Thanh-Hai","family":"Tran","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"7_CR1","unstructured":"A collection of $${\\rm TLA}^{+}$$TLA+ specifications. https:\/\/github.com\/tlaplus\/Examples\/ . Accessed 21 Oct 2017"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-33600-8_5","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"N Azmy","year":"2016","unstructured":"Azmy, N., Merz, S., Weidenbach, C.: A rigorous correctness proof for pastry. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 86\u2013101. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_5"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"7_CR5","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)"},{"issue":"4","key":"7_CR6","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"issue":"2","key":"7_CR7","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225\u2013267 (1996)","journal-title":"J. ACM"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14808-8_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA$$^{+}$$+ proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14808-8_3"},{"issue":"5","key":"7_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_55"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/978-3-642-82921-5_13","volume-title":"Control Flow and Data Flow: concepts of distributed programming","author":"EW Dijkstra","year":"1986","unstructured":"Dijkstra, E.W., Feijen, W.H., Van Gasteren, A.M.: Derivation of a termination detection algorithm for distributed computations. In: Broy, M. (ed.) Control Flow and Data Flow: concepts of distributed programming, pp. 507\u2013512. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/978-3-642-82921-5_13"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00446-002-0070-8","volume":"16","author":"E Gafni","year":"2003","unstructured":"Gafni, E., Lamport, L.: Disk paxos. Distrib. Comput. 16(1), 1\u201320 (2003)","journal-title":"Distrib. Comput."},{"issue":"2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0020-0190(00)00171-X","volume":"79","author":"R Guerraoui","year":"2001","unstructured":"Guerraoui, R.: On the hardness of failure-sensitive agreement problems. Inf. Process. Lett. 79(2), 99\u2013104 (2001)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1145\/3093333.3009860","volume":"52","author":"Igor Konnov","year":"2017","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719\u2013734 (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR15","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"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Kukovec, J., Tran, T.H., Konnov, I.: Extracting symbolic transitions from $${\\rm TLA}^{+}$$TLA+ specifications (technical report 2018). http:\/\/forsyte.at\/wp-content\/uploads\/abz2018_full.pdf . Accessed 7 Feb 2018","DOI":"10.1007\/978-3-319-91271-4_7"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM TCS 16(2), 133\u2013169 (1998)","journal-title":"ACM TCS"},{"key":"7_CR18","volume-title":"Specifying systems: the $${\\rm TLA}^{+}$$TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying systems: the $${\\rm TLA}^{+}$$TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"},{"key":"7_CR19","series-title":"Monographs in Theoretical Computer Science (An EATCS Series)","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-74107-7_8","volume-title":"Logics of specification languages","author":"S Merz","year":"2008","unstructured":"Merz, S.: The specification language $${\\rm TLA}^{+}$$TLA+. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of specification languages. Monographs in Theoretical Computer Science (An EATCS Series), pp. 401\u2013451. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74107-7_8"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-28717-6_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Merz","year":"2012","unstructured":"Merz, S., Vanzetto, H.: Automatic verification of $${\\rm TLA}^{+}$$TLA+ proof obligations with SMT solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 289\u2013303. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_23"},{"key":"7_CR21","unstructured":"Merz, S., Vanzetto, H.: Harnessing SMT solvers for $${\\rm TLA}^{+}$$TLA+ proofs. ECEASST, 53 (2012). https:\/\/hal.inria.fr\/hal-00760579"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Moraru, I., Andersen, D.G., Kaminsky, M.: There is more consensus in Egalitarian parliaments. In: SOSP, pp. 358\u2013372. ACM (2013)","DOI":"10.1145\/2517349.2517350"},{"issue":"4","key":"7_CR23","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":"7_CR24","unstructured":"Ongaro, D.: Consensus: bridging theory and practice. Ph.D. thesis, Stanford University (2014)"},{"key":"7_CR25","unstructured":"Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: HASE, pp. 209\u2013214 (1997)"},{"key":"7_CR26","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","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,17]],"date-time":"2019-10-17T12:50:34Z","timestamp":1571316634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}