{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,31]],"date-time":"2026-05-31T21:01:25Z","timestamp":1780261285311,"version":"3.54.0"},"reference-count":33,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["1031.001"],"award-info":[{"award-number":["1031.001"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80096-9","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"51-67","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":44,"title":["Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking"],"prefix":"10.1016","volume":"89","author":[{"given":"Hemanthkumar","family":"Sivaraj","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80096-9_BIB1","unstructured":"0-In Inc., http:\/\/www.0-in.com."},{"key":"10.1016\/S1571-0661(05)80096-9_BIB2","series-title":"Discrete Event Systems: Models and Applications, IIASA Conference","first-page":"40","article-title":"Distributed reachability analysis for protocol verification environments","author":"Aggarwal","year":"1987"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB3","article-title":"Distributed ltl model checking in spin","volume":"2057","author":"Barnat","year":"2001"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB4","series-title":"Proceedings of the FSTTCS Conference","article-title":"Distributed ltl model checking based on negative cycle detection","author":"Brim","year":"2001"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB5","series-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02), 1NCS","article-title":"Shared memory consistency protocol verification against weak memory models: Refinement via model checking","author":"Chatterjee","year":"2002"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB6","series-title":"\u201cModel Checking,\u201d","author":"Clarke","year":"1999"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB7","series-title":"International Conference on Software Engineering","first-page":"439","article-title":"Bandera: extracting finite-state models from java source code","author":"Corbett","year":"2000"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB8","first-page":"275","volume":"1","author":"Courcoubetis","year":"1992","journal-title":"Memory efficient algorithms for the verification of temporal properties"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB9","first-page":"390","article-title":"The murphi verification system","volume":"1102","author":"Dill","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB10","series-title":"IEEE Transactions on Software Engineering 27","first-page":"99","article-title":"Dynamically discovering likely program invariants to support program evolution","author":"Ernst","year":"2001"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB11","series-title":"Efficient distributed sat and satbased distributed bounded model checking, to Appear in the Charme 2003 Conference","author":"Ganani","year":"2003"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB12","series-title":"Parallel Computing 22","first-page":"789","article-title":"High-performance, portable implementation of the MPI Message Passing Interface Standard","author":"Gropp","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB13","series-title":"International Conference on Computer Aided Verification","article-title":"Distributed symbolic model checking for the mu-calculus","author":"Grumberg","year":"2001"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB14","series-title":"Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","first-page":"74","article-title":"Discovering affine equalities using random interpretation","author":"Gulwani","year":"2003"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB15","series-title":"Proceedings of ECSEL Workshop","article-title":"Model checking by random walk","author":"Haslum","year":"1999"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB16","first-page":"20","article-title":"Achieving scalability in parallel reachability analysis of very large circuits, 12th International Conference on Computer Aided Verification","volume":"1855","author":"Heyman","year":"2000","journal-title":"LNCS"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB17","series-title":"Proceedings of 2nd SPIN Workshop","article-title":"On nested depth-first search","author":"Holzmann","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB19","series-title":"Technical Report FV-001, Laboratory for Applied Logic, Brigham Young University","article-title":"Using idle workstations to find ltl property violations","author":"Jones","year":"2002"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB20","series-title":"European Design Automation Conference","first-page":"514","article-title":"Finite state machine verification on mimd machines","author":"Kumar","year":"1992"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB21","series-title":"Calculational System Design","article-title":"Specifying concurrent systems with TLA+","author":"Lamport","year":"1999"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB22","article-title":"Distributed-memory model checking with spin","volume":"1680","author":"Lerda","year":"1999"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB23","first-page":"132","article-title":"On the random walk method of protocol testing, Proceedings of the 5th Workshop on Computer Aided Verification","volume":"818","author":"Mihail","year":"1994","journal-title":"LNCS"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB24","series-title":"Proceedings of the 38th Design Automation Conference (DAC'01)","article-title":"Chaff: Engineering an Efficient SAT Solver","author":"Moskewicz","year":"2001"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB25","series-title":"\u201cParallel Programming with MPI,\u201d Morgan Kaufmann, iSBN 1-55860-339-5","author":"Pacheco","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB26","series-title":"International Conference on Computer Design","first-page":"358","article-title":"Binary decision diagrams on network of workstations","author":"Ranjan","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB27","first-page":"229","volume":"20","author":"Reif","year":"1985","journal-title":"Depth-first search is inherently sequential"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB28","series-title":"Computer Aided Verification","first-page":"256","article-title":"Parallelizing the murphi verifier","author":"Stern","year":"1997"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB29","series-title":"\u201cImplementation of an efficient parallel BDD package,\u201d Master's thesis, University of California at Santa Barbara","author":"Stornetta","year":"1995"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB30","series-title":"33rd Design Automation Conference","first-page":"641","article-title":"Implementation of an efficient parallel bdd package","author":"Stornetta","year":"1996"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB31","series-title":"Proceedings of the Third International Workshop on High-Level Parallel Programming Models and Supportive Environments (HIPS'98)","article-title":"Making distributed shared memory simple, yet efficient","author":"Swanson","year":"1998"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB32","series-title":"Java pathfinder - second generation of a java model checker","author":"Visser","year":"2000"},{"key":"10.1016\/S1571-0661(05)80096-9_BIB33","series-title":"Symposium Proceedings on Communications Architecture and Protocols","first-page":"303","article-title":"Protocol validation in complex systems","author":"West","year":"1989"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800969?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800969?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,5,31]],"date-time":"2026-05-31T20:07:17Z","timestamp":1780258037000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800969"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800969"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80096-9","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80096-9","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}