{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:54:36Z","timestamp":1725544476530},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_7","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:14:13Z","timestamp":1143537253000},"page":"108-125","source":"Crossref","is-referenced-by-count":10,"title":["Parallel and Distributed Model Checking in Eddy"],"prefix":"10.1007","author":[{"given":"Igor","family":"Melatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Palmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey","family":"Sawaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert Mike","family":"Kirby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1008771324652","volume":"18","author":"U. Stern","year":"2001","unstructured":"Stern, U., Dill, D.: Parallelizing the Mur\u03c6 verifier. Formal Methods in System Design\u00a018(2), 117\u2013129 (2001); Journal version of their CAV paper","journal-title":"Formal Methods in System Design"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 22. Springer, Heidelberg (1999)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The murphi verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"key":"7_CR4","volume-title":"Programming with POSIX Threads","author":"D.R. Butenhof","year":"1997","unstructured":"Butenhof, D.R.: Programming with POSIX Threads. Addison-Wesley, Reading (1997)"},{"key":"7_CR5","unstructured":"POSIX PThreads, http:\/\/www.llnl.gov\/computing\/tutorials\/pthreads\/"},{"key":"7_CR6","unstructured":"MPI tutorial, http:\/\/www-unix.mcs.anl.gov\/mpi\/tutorial\/gropp\/talk.html"},{"key":"7_CR7","unstructured":"PThreads Win32 home page, http:\/\/sourceware.org\/pthreads-win32\/"},{"key":"7_CR8","unstructured":"MCCS (2003), http:\/\/www.microsoft.com\/windowsserver2003\/ccs\/overview.mspx"},{"key":"7_CR9","unstructured":"Palmer, R., Gopalakrishnan, G.: Refactoring spin for safety. Technical report, University of Utah (July 2005)"},{"issue":"4","key":"7_CR10","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G. Penna Della","year":"2004","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M.: Exploiting transition locality in automatic verification of finite state concurrent systems. Software Tools for Technology Transfer\u00a06(4), 320\u2013341 (2004)","journal-title":"Software Tools for Technology Transfer"},{"key":"7_CR11","unstructured":"Eddy Murphi distribution, http:\/\/www.cs.utah.edu\/formal_verification\/software\/murphi\/eddy_murphi\/"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11560548_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"key":"7_CR13","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"75","volume-title":"Proc. of PDMC 2004","author":"Y. Feldman","year":"2005","unstructured":"Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: Design and implementation. In: Proc. of PDMC 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0128(3), pp. 75\u201390. Elsevier, Amsterdam (2005)"},{"key":"7_CR14","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"3","volume-title":"Proc. of PDMC 2003","author":"R. Kumar","year":"2003","unstructured":"Kumar, R., Mercer, E.: Scalable distributed model checking: Experiences, lessons, and expectations. In: Proc. of PDMC 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a089(1), p. 3. Elsevier, Amsterdam (2003)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-60385-9_2","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Automatic verification of the sci cache coherence protocol. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 21\u201334. Springer, Heidelberg (1995)"},{"key":"7_CR16","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"51","volume-title":"Proc. of PDMC 2003","author":"H. Sivaraj","year":"2003","unstructured":"Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proc. of PDMC 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a089(1), pp. 51\u201367. Elsevier, Amsterdam (2003)"},{"key":"7_CR17","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"19","volume-title":"Proc. of PDMC 2004","author":"R. Kumar","year":"2004","unstructured":"Kumar, R., Mercer, E.: Load balancing parallel explicit state model checking. In: Proc. of PDMC 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0128(3), pp. 19\u201334. Elsevier, Amsterdam (2004)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. Technical report, Microsoft Research (2004)","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"7_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/7056.001.0001","volume-title":"Using MPI: Portable Parallel Programming with the Message-Passing Interface","author":"W. Gropp","year":"1999","unstructured":"Gropp, W., Lusk, E., Skjellum, A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge (1999)"},{"key":"7_CR20","unstructured":"MPI official specification, http:\/\/www.mpi-forum.org\/docs\/docs.html"},{"key":"7_CR21","unstructured":"Murphi distribution, http:\/\/sprout.stanford.edu\/dill\/murphi.html"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Stern, U., Dill, D.: Parallelizing the mur\u03d5 verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Kuskin, J., Ofelt, D., et al.: The Stanford FLASH multiprocessor. In: Proc. of SIGARCH 1994, May 1994, pp. 302\u2013313 (1994)","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"1","key":"7_CR24","first-page":"270","volume":"3","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. Software Tools for Technology Transfer\u00a03(1), 270\u2013278 (1998)","journal-title":"Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T13:18:54Z","timestamp":1555507134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11691617_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}