{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T23:28:23Z","timestamp":1720999703107},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,4,6]],"date-time":"2004-04-06T00:00:00Z","timestamp":1081209600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10009-003-0126-5","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T08:17:12Z","timestamp":1081325832000},"page":"67-76","source":"Crossref","is-referenced-by-count":9,"title":["Using simulated execution in verifying distributed algorithms"],"prefix":"10.1007","volume":"6","author":[{"given":"Toh Ne","family":"Win","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen J.","family":"Garland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilsun","family":"K\u0131rl\u0131","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy A.","family":"Lynch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,6]]},"reference":[{"key":"126_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S (1998) Mocha: Exploiting modularity in model checking. In: Proceedings of the 10th international conference on computer-aided verification, Vancouver, BC, Canada, 28 June\u20132 July 1998. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 521\u2013525","DOI":"10.1007\/BFb0028774"},{"key":"126_CR2","unstructured":"Bogdanov A (2000) Formal verification of simulations between I\/O automata. Master of engineering thesis, Massachusetts Institute of Technology, Cambridge, MA"},{"key":"126_CR3","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0304-3975(00)00042-6","volume":"243","author":"De","year":"2000","unstructured":"De Prisco R, Lampson B, Lynch N (2000) Fundamental study: revisiting the Paxos algorithm. Theor Comput Sci 243:35\u201391","journal-title":"Theor Comput Sci"},{"key":"126_CR4","first-page":"Proceedings","volume":"in","author":"Ernst","year":"1999","unstructured":"Ernst MD, Cockrell J, Griswold WG, Notkin D (1999) Dynamically discovering likely program invariants to support program evolution. IEEE Trans Softw Eng 27(2):1\u201325. A previous version appeared in: Proceedings of the 21st international conference on software engineering (ICSE \u201999), Los Angeles, 19\u201321 May 1999, pp 213\u2013224","journal-title":"A previous version appeared"},{"key":"126_CR5","doi-asserted-by":"crossref","unstructured":"Ernst MD, Czeisler A, Griswold WG, Notkin D (2000) Quickly detecting relevant program invariants. In: Proceedings of the 22nd international conference on software engineering (ICSE 2000), Limerick, Ireland, 7\u20139 June 2000, pp 449\u2013458","DOI":"10.1109\/ICSE.2000.870435"},{"key":"126_CR6","unstructured":"Garland S, Guttag J (1991) A guide to LP, the Larch Prover. Technical report, DEC Systems Research Center, Palo Alto, CA, December 31. Updated version available at: http:\/\/nms.lcs.mit.edu\/Larch\/LP"},{"key":"126_CR7","unstructured":"Garland SJ, Lynch NA (1998) The IOA language and toolset: support for designing, analyzing, and building distributed systems. Technical Report MIT\/LCS\/TR-762, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, August 1998. http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/IOA-TR-762.ps"},{"key":"126_CR8","unstructured":"Gordon MJC (1989) HOL: a proof generating system for higher order logic. In: Birtwistle G, Subrahmanyam PA (eds) Current trends in hardware verification and automated theorem proving. Springer, Berlin Heidelberg New York, pp 73\u2013128"},{"key":"126_CR9","unstructured":"Gurevich Y, Schulte W, Veanes M (2001) Toward industrial strength abstract state machines. Technical Report MSR-TR-2001-98, Microsoft Research, 2001. Software available at: http:\/\/www.research.microsoft.com\/foundations\/asml\/"},{"key":"126_CR10","doi-asserted-by":"crossref","unstructured":"Guttag JV, Horning JJ, Garland SJ, Jones KD, Modet A, Wing JM (1993) Larch: languages and tools for formal specification. In: Texts and monographs in computer science. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"126_CR11","unstructured":"K\u0131rl\u0131 D, Chefter A, Dean L, Garland SJ, Lynch NA, Ne Win T, Ramirez-Robredo A (2002a) The IOA simulator. Technical Report MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, MA, July 2002"},{"key":"126_CR12","unstructured":"K\u0131rl\u0131 D, Chefter A, Dean L, Garland SJ, Lynch NA, Ne Win T, Ramirez-Robredo A (2002b) Simulating nondeterministic systems at multiple levels of abstraction. In: Proceedings of Tools Day 2002, Brno, Czech Republic, August 2002, pp 44\u201359. Also available as Masaryk University Technical Report FI MU-RS-2002-05"},{"key":"126_CR13","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"Lamport","year":"1998","unstructured":"Lamport L (1998) The part-time parliament. ACM Trans Comput Sys 16(2):133\u2013169","journal-title":"ACM Trans Comput Sys"},{"key":"126_CR14","unstructured":"Lamport L, Yu Y (2001) TLC \u2013 The TLA+ model checker. Compaq Systems Research Center, Palo Alto, CA, 2001. http:\/\/research.microsoft.com\/users\/lamport\/tla\/tlc.html"},{"key":"126_CR15","unstructured":"Lynch N (1996) Distributed algorithms. Morgan Kaufmann, San Mateo, CA"},{"key":"126_CR16","unstructured":"Lynch NA, Tuttle MR (1989) An introduction to Input\/Output automata. CWI-Q 2(3):219\u2013246"},{"key":"126_CR17","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"Lynch","year":"1995","unstructured":"Lynch N, Vaandrager F (1995) Forward and backward simulations: Part I. Untimed systems. Inf Comput 121(2):214\u2013233","journal-title":"Inf Comput"},{"key":"126_CR18","unstructured":"McMillan KL (1998) The SMV language. Cadence Berkeley Labs, 2001 Addison Street, Berkeley, CA. http:\/\/www.cis.ksu.edu\/santos\/smv-doc\/"},{"key":"126_CR19","doi-asserted-by":"crossref","unstructured":"Nimmer JW, Ernst MD (2002a) Automatic generation of program specifications. In: Proceedings of the 2002 international symposium on software testing and analysis (ISSTA), Rome, Italy, 22\u201324 July 2002, pp 232\u2013242","DOI":"10.1145\/566172.566213"},{"key":"126_CR20","doi-asserted-by":"crossref","unstructured":"Nimmer JW, Ernst MD (2002b) Invariant inference for static checking: An empirical evaluation. In: Proceedings of the ACM SIGSOFT 10th international symposium on the foundations of software engineering (FSE 2002), Charleston, SC, 20\u201322 November 2002, pp 11\u201320","DOI":"10.1145\/605466.605469"},{"key":"126_CR21","unstructured":"Paulson LC (1993) The Isabelle reference manual. Technical Report 283, Cambridge University, Computer Laboratory, Cambridge, UK"},{"key":"126_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli A, Ruah S, Zuck L (2001) Automatic deductive verification with invisible invariants. In: Proceedings of the conference on tools and algorithms for the analysis and construction of systems (TACAS), Genoa, Italy, 2\u20136 April 2001. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 82\u201397","DOI":"10.1007\/3-540-45319-9_7"},{"key":"126_CR23","unstructured":"Rintanen J (2000) An iterative algorithm for synthesizing invariants. In: Proceedings of the 17th national conference on artificial intelligence and the 12th conference on innovative applications of artificial intelligence, Austin, TX, 30 July\u20133 August 2000, pp 806\u2013811"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0126-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0126-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0126-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:18Z","timestamp":1559114718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0126-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,6]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["126"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0126-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,6]]}}}