{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:34:17Z","timestamp":1694633657532},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2003,11,1]],"date-time":"2003-11-01T00:00:00Z","timestamp":1067644800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. & Technol."],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/bf02945465","type":"journal-article","created":{"date-parts":[[2008,9,7]],"date-time":"2008-09-07T16:27:34Z","timestamp":1220804854000},"page":"762-770","source":"Crossref","is-referenced-by-count":9,"title":["Combining static analysis and case-based search space partitioning for reducing peak memory in model checking"],"prefix":"10.1007","volume":"18","author":[{"given":"WenHui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02945465_CR1","first-page":"428","volume":"5","author":"J R Burch","year":"1990","unstructured":"Burch J R, Clarke E M, McMillan K L,et al. Symbolic model checking: 1020 states and beyondIEEE Symposium on Logic in Computer Science, 1990, 5: 428\u2013439.","journal-title":"IEEE Symposium on Logic in Computer Science"},{"key":"BF02945465_CR2","doi-asserted-by":"crossref","unstructured":"Enders R, Filkorn T, Taubner D. Generating BDDs for symbolic model checking in CCS.Lecture Notes in Computer Science 575, CAV, 1991, pp. 203\u2013213.","DOI":"10.1007\/3-540-55179-4_20"},{"issue":"4","key":"BF02945465_CR3","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari A. A stubborn attack on state explosion.Formal Methods in System Design, December 1992, 1(4): 297\u2013322.","journal-title":"Formal Methods in System Design"},{"key":"BF02945465_CR4","doi-asserted-by":"crossref","unstructured":"Emerson E A, Sistla A P. Symmetry and model checking.Lecture Notes in Computer Science 697,CAV, 1993, pp. 463\u2013478.","DOI":"10.1007\/3-540-56922-7_38"},{"issue":"5","key":"BF02945465_CR5","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E M Clarke","year":"1994","unstructured":"Clarke E M, Grumberg O, Long D E. Model checking and abstraction.ACM Trans. Programming Languages and Systems, 1994, 16(5): 1512\u20131542.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"BF02945465_CR6","first-page":"1","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux C, Graf S, Sifakis Jet al. Property preserving abstractions for the verification of concurrent systems.J. Formal Methods in System Design, 1995, 6: 1\u201335.","journal-title":"J. Formal Methods in System Design"},{"key":"BF02945465_CR7","doi-asserted-by":"crossref","unstructured":"Manku G S, Hojati R, Brayton R K. Structural symmetry and model checking.Lecture Notes in Computer Science 1427, Vancouver, CanadaCAV, 1998, pp. 159\u2013171.","DOI":"10.1007\/BFb0028742"},{"key":"BF02945465_CR8","volume-title":"Design and Validation of Computer Protocols","author":"G J Holzmann","year":"1991","unstructured":"Holzmann G J. Design and Validation of Computer Protocols. Prentice Hall, New Jersey, 1991."},{"issue":"1","key":"BF02945465_CR9","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H R Andersen","year":"1994","unstructured":"Andersen H R. Model checking and Boolean graphs.Theoretical Computer Science, 1994, 126(1): 3\u201313.","journal-title":"Theoretical Computer Science"},{"key":"BF02945465_CR10","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF02252682","volume":"6","author":"S Katz","year":"1992","unstructured":"Katz S, Peled D. Verification of distributed programs using representative interleaving sequences.Distributed Computing, 1992, 6: 107\u2013120.","journal-title":"Distributed Computing"},{"key":"BF02945465_CR11","doi-asserted-by":"crossref","unstructured":"Peled D. All from one, one for all, on model-checking using representatives.Lecture Notes in Computer Science 697,CAV, 1993, pp. 409\u2013423.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"BF02945465_CR12","doi-asserted-by":"crossref","unstructured":"Peled D. Ten years of partial order reduction.Lecture Notes in Computer Science 1427, Vancouver, Canada,CAV, 1998, pp. 17\u201328.","DOI":"10.1007\/BFb0028727"},{"issue":"5","key":"BF02945465_CR13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G J Holzmann","year":"1997","unstructured":"Holzmann G J. The model checker Spin.IEEE Trans. Software Engineering, May 1997, 23(5): 279\u2013295.","journal-title":"IEEE Trans. Software Engineering"},{"key":"BF02945465_CR14","doi-asserted-by":"crossref","unstructured":"Berezin S, Campos S, Clarke E M. Compositional reasoning in model checking.Lecture Notes in Computer Science 1536, COMPOS, 1997, pp 81\u2013102.","DOI":"10.1007\/3-540-49213-5_4"},{"issue":"4","key":"BF02945465_CR15","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s100090050041","volume":"2","author":"L I Millett","year":"2000","unstructured":"Millett L I, Teitelbaum T. Issues in slicing PROMELA and its applications to model checking protocol understanding, and simulation.STTT, 2000, 2(4): 343\u2013349.","journal-title":"STTT"},{"key":"BF02945465_CR16","doi-asserted-by":"crossref","unstructured":"Emerson E A. Temporal and modal logic.Handbook of Theoretical Computer Science, 1990, (B): 997\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"BF02945465_CR17","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled D, Vardi M, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In15th IFIP WG6.1 Int. Symp. Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"BF02945465_CR18","doi-asserted-by":"crossref","unstructured":"Bloem R, Ravi K, Somenzi F. Efficient decision procedures for model checking of linear time logic properties.Lecture Notes in Computer Science 1633, Trento, Italy,CAV, 1999, pp. 222\u2013235.","DOI":"10.1007\/3-540-48683-6_21"},{"key":"BF02945465_CR19","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R. Efficient B\u00fcchi automata from LTL formulae.Lecture Notes in Computer Science 1855, Chicago, USA, CAV, 2000, pp. 248\u2013263.","DOI":"10.1007\/10722167_21"},{"key":"BF02945465_CR20","doi-asserted-by":"crossref","unstructured":"Stahl K, Baukus K, Lakhnech Yet al. Divide, abstract, and model-check.Lecture Notes in Computer Science 1680, InProc. the 5th International SPIN Workshop, Trento, Italy, July 1999, pp. 57\u201376.","DOI":"10.1007\/3-540-48234-2_5"},{"key":"BF02945465_CR21","doi-asserted-by":"crossref","unstructured":"Hoare C A R. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"BF02945465_CR22","doi-asserted-by":"crossref","unstructured":"Zhang W. A strategy for improving the efficiency of procedure verification.Lecture Notes in Computer Science, 2434, Catania, Italy, SAFECOMP, 2002, pp. 113\u2013126.","DOI":"10.1007\/3-540-45732-1_13"},{"key":"BF02945465_CR23","doi-asserted-by":"crossref","unstructured":"Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR,Lecture Notes in Computer Science 1055, TAGAS, 1996, pp. 147\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"BF02945465_CR24","doi-asserted-by":"crossref","unstructured":"Crazzolara F, Winskel G. Petri nets in cryptographic protocols. InProc. the 15th Int. Parallel and Distributed Processing Symp., IEEE-IPDPS-01, 2001, pp. 149\u2013157.","DOI":"10.1109\/IPDPS.2001.925135"},{"key":"BF02945465_CR25","doi-asserted-by":"crossref","unstructured":"McMillan K L. Verification of infinite state systems by compositional model checking.Lecture Notes in Computer Science 1703, CHARME, 1999, pp. 219\u2013234.","DOI":"10.1007\/3-540-48153-2_17"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02945465.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02945465\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02945465","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T02:34:54Z","timestamp":1631759694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02945465"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,11]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["BF02945465"],"URL":"https:\/\/doi.org\/10.1007\/bf02945465","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,11]]}}}