{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:33:39Z","timestamp":1742402019209},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,11,12]],"date-time":"2008-11-12T00:00:00Z","timestamp":1226448000000},"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":[[2009,2]]},"DOI":"10.1007\/s10009-008-0094-x","type":"journal-article","created":{"date-parts":[[2008,11,11]],"date-time":"2008-11-11T03:43:51Z","timestamp":1226375031000},"page":"13-25","source":"Crossref","is-referenced-by-count":17,"title":["Parallel and distributed model checking in Eddy"],"prefix":"10.1007","volume":"11","author":[{"given":"I.","family":"Melatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Palmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Sawaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. M.","family":"Kirby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,11,12]]},"reference":[{"key":"94_CR1","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.: Parallelizing the Mur $${\\phi}$$ verifier. Form Methods Sys Des 18(2), 117\u2013129 (2001) (Journal version of their CAV 1997 paper)","DOI":"10.1023\/A:1008771324652"},{"key":"94_CR2","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN 1999, Lecture Notes in Computer Science, vol. 1680. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48234-2_3"},{"key":"94_CR3","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: The mur phi verification system. In: Proceedings of CAV 1996, Lecture Notes in Computer Science, vol. 1102, pp. 390\u2013393. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61474-5_86"},{"key":"94_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":"94_CR5","unstructured":"POSIX PThreads http:\/\/www.llnl.gov\/computing\/tutorials\/pthreads\/"},{"key":"94_CR6","unstructured":"MPI tutorial http:\/\/www-unix.mcs.anl.gov\/mpi\/tutorial\/gropp\/talk.html"},{"key":"94_CR7","unstructured":"PThreads Win32 home page http:\/\/sourceware.org\/pthreads-win32\/"},{"key":"94_CR8","unstructured":"MCCS 2003 http:\/\/www.microsoft.com\/windowsserver2003\/ccs\/overview.mspx"},{"key":"94_CR9","unstructured":"Palmer, R., Gopalakrishnan, G.: Refactoring spin for safety. Technical report, University of Utah, July 2005"},{"issue":"4","key":"94_CR10","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G. Della Penna","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. Softw Tools Technol Transf 6(4), 320\u2013341 (2004)","journal-title":"Softw Tools Technol Transf"},{"key":"94_CR11","unstructured":"Eddy_Murphi distribution http:\/\/www.cs.utah.edu\/formal_verification\/software\/murphi\/eddy_murphi"},{"key":"94_CR12","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Proceedings of CHARME 2005, Lecture Notes in Computer Science, vol. 3725, pp. 129\u2013145. Springer, Heidelberg (2005)","DOI":"10.1007\/11560548_12"},{"key":"94_CR13","doi-asserted-by":"crossref","unstructured":"Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: design and implementation. In: Proceedings of PDMC 2004, Electronic Notes in Theoretical Computer Science, vol. 128(3), pp. 75\u201390. Elsevier, Amsterdam (2005)","DOI":"10.1016\/j.entcs.2004.10.020"},{"key":"94_CR14","doi-asserted-by":"crossref","unstructured":"Kumar, R., Mercer, E.: Scalable distributed model checking: experiences, lessons, and expectations. In: Proceedings of PDMC 2003, Electronic Notes in Theoretical Computer Science, vol. 89(1), p. 3. Elsevier, Amsterdam (2003)","DOI":"10.1016\/S1571-0661(05)80092-1"},{"key":"94_CR15","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Automatic verification of the sci cache coherence protocol. In: Proceedings of CHARME 1995, Lecture Notes in Computer Science, vol. 987, pp. 21\u201334. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60385-9_2"},{"key":"94_CR16","doi-asserted-by":"crossref","unstructured":"Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proceedings of PDMC 2003, Electronic Notes in Theoretical Computer Science, vol. 89(1), pp. 51\u201367. Elsevier, Amsredam (2003)","DOI":"10.1016\/S1571-0661(05)80096-9"},{"key":"94_CR17","doi-asserted-by":"crossref","unstructured":"Kumar, R., Mercer, E.: Load balancing parallel explicit state model checking. In: Proceedings. of PDMC 2004, Electronic Notes in Theoretical Computer Science, vol. 128 (3), pp. 19\u201334. Elsevier (2004)","DOI":"10.1016\/j.entcs.2004.10.016"},{"key":"94_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":"94_CR19","doi-asserted-by":"crossref","unstructured":"Gropp, W., Lusk, E., Skjellum, A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press (1999)","DOI":"10.7551\/mitpress\/7056.001.0001"},{"key":"94_CR20","unstructured":"MPI official specification http:\/\/www.mpi-forum.org\/docs\/docs.html"},{"key":"94_CR21","unstructured":"Murphi distribution http:\/\/sprout.stanford.edu\/dill\/murphi.html"},{"key":"94_CR22","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.: Parallelizing the mur\u03c6 verifier. In: Grumberg, O. (ed.) Proceedings. of CAV 1997, Lecture Notes in Computer Science, vol. 1254, pp. 256\u2013278. Springer (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"94_CR23","doi-asserted-by":"crossref","unstructured":"Kuskin, J., Ofelt, D. et al.: The Stanford FLASH multiprocessor. In: Proceedings. of SIGARCH 1994, pp. 302\u2013313, May 1994","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"1","key":"94_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 3(1), 270\u2013278 (1998)","journal-title":"Software Tools for Technology Transfer"}],"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-008-0094-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0094-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0094-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:24Z","timestamp":1559100324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0094-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,12]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["94"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0094-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,12]]}}}