{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:47:44Z","timestamp":1725727664084},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385919"},{"type":"electronic","value":"9783642385926"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38592-6_2","type":"book-chapter","created":{"date-parts":[[2013,5,29]],"date-time":"2013-05-29T00:56:11Z","timestamp":1369788971000},"page":"5-19","source":"Crossref","is-referenced-by-count":2,"title":["Formal Analysis of a Distributed Algorithm for Tracking Progress"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[]},{"given":"Frank","family":"McSherry","sequence":"additional","affiliation":[]},{"given":"Derek G.","family":"Murray","sequence":"additional","affiliation":[]},{"given":"Thomas L.","family":"Rodeheffer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"issue":"1","key":"2_CR2","doi-asserted-by":"crossref","first-page":"241","DOI":"10.14778\/1687627.1687655","volume":"2","author":"B. Chandramouli","year":"2009","unstructured":"Chandramouli, B., Goldstein, J., Maier, D.: On-the-fly progress detection in iterative stream queries. Proc. VLDB Endow.\u00a02(1), 241\u2013252 (2009)","journal-title":"Proc. VLDB Endow."},{"key":"2_CR3","first-page":"305","volume-title":"Developments in Concurrency and Communication","author":"K.M. Chandy","year":"1990","unstructured":"Chandy, K.M., Misra, J.: Proofs of distributed algorithms: An exercise. In: Hoare, C.A.R. (ed.) Developments in Concurrency and Communication, pp. 305\u2013332. Addison-Wesley, Boston (1990)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the tLA\u2009+\u2009 proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 142\u2013148. Springer, Heidelberg (2010)"},{"issue":"3","key":"2_CR5","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/3916.3988","volume":"7","author":"D.R. Jefferson","year":"1985","unstructured":"Jefferson, D.R.: Virtual time. ACM Trans. Program. Lang. Syst.\u00a07(3), 404\u2013425 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Lamport, L.: The TLA Toolbox, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/toolbox.html","key":"2_CR6"},{"key":"2_CR7","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"2_CR8","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 TLA\u2009+\u2009 proof obligations with SMT solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 289\u2013303. Springer, Heidelberg (2012)"},{"unstructured":"Naiad: Web page, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/projects\/naiad\/","key":"2_CR9"},{"unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)","key":"2_CR10"},{"unstructured":"Rodeheffer, T.L.: The Naiad clock protocol: Specification, model checking, and correctness proof. Tech. Rep. MSR-TR-2013-20, Microsoft Research, Redmond (February 2013), \n                    \n                      http:\/\/research.microsoft.com\/apps\/pubs\/?id=183826","key":"2_CR11"},{"unstructured":"Samadi, B.: Distributed Simulation, Algorithms and Performancs Analysis. Ph.D. thesis, University of California, Los Angeles (1985), Tech. Rep. CSD-850006, \n                    \n                      http:\/\/ftp.cs.ucla.edu\/tech-report\/198_-reports\/850006.pdf","key":"2_CR12"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1109\/TKDE.2003.1198390","volume":"15","author":"P.A. Tucker","year":"2003","unstructured":"Tucker, P.A., Maier, D., Sheard, T., Fegaras, L.: Exploiting punctuation semantics in continuous data streams. IEEE Trans. Knowl. Data Eng.\u00a015(3), 555\u2013568 (2003)","journal-title":"IEEE Trans. Knowl. Data Eng."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38592-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:48:51Z","timestamp":1558302531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38592-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385919","9783642385926"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38592-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}