{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:21:20Z","timestamp":1740133280622,"version":"3.37.3"},"reference-count":33,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61370072","61073033"],"award-info":[{"award-number":["61370072","61073033"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Australian Research Council Discovery","award":["DP110101211"],"award-info":[{"award-number":["DP110101211"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. VLSI Syst."],"published-print":{"date-parts":[[2015,5]]},"DOI":"10.1109\/tvlsi.2014.2330061","type":"journal-article","created":{"date-parts":[[2014,10,6]],"date-time":"2014-10-06T15:08:34Z","timestamp":1412608114000},"page":"905-915","source":"Crossref","is-referenced-by-count":6,"title":["An I\/O Efficient Model Checking Algorithm for Large-Scale Systems"],"prefix":"10.1109","volume":"23","author":[{"given":"Lijun","family":"Wu","sequence":"first","affiliation":[]},{"given":"Huijia","family":"Huang","sequence":"additional","affiliation":[]},{"given":"Kaile","family":"Su","sequence":"additional","affiliation":[]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[]},{"given":"Xiaosong","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"year":"2013","journal-title":"Hard Disk Drive","key":"ref33"},{"key":"ref32","first-page":"640","article-title":"STXXL: Standard template library for XXL data sets","volume":"3669","author":"dementiev","year":"2005","journal-title":"Proc Ann European Symp Algorithms (ESA)"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/11817963_26","article-title":"DiVinE: A tool for distributed verification","volume":"4144","author":"barnat","year":"2006","journal-title":"Proc 18th Int Conf Comput Aided Verificat (CAV)"},{"doi-asserted-by":"publisher","key":"ref30","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"616","DOI":"10.1007\/978-3-642-22110-1_50","article-title":"Fully symbolic model checking for timed automata","author":"morb\u00e9","year":"2011","journal-title":"Proc 23rd Int Conf Comput Aided Verificat (CAV)"},{"key":"ref11","first-page":"1","author":"holzmann","year":"2004","journal-title":"The SPIN Model Checker Primer and Reference Manual"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Adv Comput"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1145\/1455248.1455250"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1007\/978-3-540-73368-3_32"},{"key":"ref15","article-title":"Parallel external directed model checking with linear I\/O","author":"jabbar","year":"2006","journal-title":"Proc 7th Int Conf Verificat Model Check Abstract Interpret (VMCAI)"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","article-title":"Memory efficient algorithms for the verification of temporal properties","volume":"1","author":"courcoubetis","year":"1990","journal-title":"Formal Methods Syst Design"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","article-title":"Accepting predecessors are better than back edges in distributed LTL model-checking","volume":"3312","author":"brim","year":"2004","journal-title":"Proc 5th Int Conf Formal Methods Comput -Aided Design (FMCAD)"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","article-title":"Semi-external LTL model checking","author":"edelkamp","year":"2008","journal-title":"Proc Int Conf Comput Aided Verificat (CAV)"},{"year":"1999","journal-title":"ITC’99","key":"ref19"},{"key":"ref28","first-page":"49","article-title":"Distributed explicit fair cycle detection","volume":"2648","author":"cerna","year":"2003","journal-title":"Proc SPIN"},{"key":"ref4","first-page":"154","article-title":"Hardware model checking: Status, challenges, and opportunities","author":"talupur","year":"2011","journal-title":"Proc Int Conf Formal Methods Comput -Aided Design (FMCAD)"},{"doi-asserted-by":"publisher","key":"ref27","DOI":"10.1007\/978-3-540-78800-3_5"},{"doi-asserted-by":"publisher","key":"ref3","DOI":"10.1109\/TCAD.2005.850814"},{"key":"ref6","first-page":"438","article-title":"Refining dependencies improves partial-order verification methods","author":"godefroid","year":"1993","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref29","first-page":"332","article-title":"A functional approach to external graph algorithms","author":"abello","year":"1998","journal-title":"Proceedings of the 6th annual European Symposium on Algorithms (ESA)"},{"key":"ref5","first-page":"121","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref8","first-page":"1512","article-title":"Model checking and abstraction","volume":"16","author":"clarke","year":"1993"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"616","DOI":"10.1007\/978-3-642-31424-7_43","article-title":"A complete method for symmetry reduction in safety verification","author":"chu","year":"2012","journal-title":"Proc Int Conf Comput Aided Verificat (CAV)"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1109\/TVLSI.2003.812320"},{"key":"ref9","first-page":"239","article-title":"Compositional state space generation from Lotos programs","author":"krimm","year":"1997","journal-title":"Proc Tools Algorithms the Construction Anal Syst (TACAS)"},{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1016\/S0167-6423(99)00030-1"},{"doi-asserted-by":"publisher","key":"ref20","DOI":"10.1145\/48529.48535"},{"key":"ref22","first-page":"650","article-title":"Best-first frontier search with delayed duplicate detection","author":"korf","year":"2004","journal-title":"Proc 19th Nat Conf Artif Intell (AAAI)"},{"key":"ref21","first-page":"172","article-title":"Using magnetic disk instead of main memory in the Mur $\\varphi $ verifier","author":"stern","year":"1998","journal-title":"Proc 10th Int Conf Comput Aided Verificat (CAV)"},{"key":"ref24","first-page":"723","article-title":"External-memory breadth-first search with sublinear I\/O","author":"mehlhorn","year":"2002","journal-title":"Proc Ann European Symp Algorithms (ESA)"},{"key":"ref23","first-page":"1380","article-title":"Large-scale parallel breadth-first search","author":"korf","year":"2005","journal-title":"Proc 20th Nat Conf Artif Intell (AAAI 2005)"},{"doi-asserted-by":"publisher","key":"ref26","DOI":"10.1109\/ASE.2003.1240299"},{"key":"ref25","first-page":"1","article-title":"Large-scale directed model checking LTL","author":"edelkamp","year":"2006","journal-title":"Proc SPIN"}],"container-title":["IEEE Transactions on Very Large Scale Integration (VLSI) Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/92\/7091984\/06850009.pdf?arnumber=6850009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:28:54Z","timestamp":1642004934000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/6850009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5]]},"references-count":33,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/tvlsi.2014.2330061","relation":{},"ISSN":["1063-8210","1557-9999"],"issn-type":[{"type":"print","value":"1063-8210"},{"type":"electronic","value":"1557-9999"}],"subject":[],"published":{"date-parts":[[2015,5]]}}}