{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T09:44:41Z","timestamp":1648719881213},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Ser. F-Inf. Sci."],"published-print":{"date-parts":[[2007,12]]},"DOI":"10.1007\/s11432-007-0073-y","type":"journal-article","created":{"date-parts":[[2007,11,17]],"date-time":"2007-11-17T09:41:41Z","timestamp":1195292501000},"page":"793-810","source":"Crossref","is-referenced-by-count":1,"title":["Combining search space partition and abstraction for LTL model checking"],"prefix":"10.1007","volume":"50","author":[{"given":"Fei","family":"Pu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"WenHui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"73_CR1","volume-title":"Model Checking","author":"E. M. Clark","year":"1999","unstructured":"Clark E M, Grumberg O, Peled D et al. Model Checking. Cambridge, MA: The MIT Press, 1999"},{"key":"73_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proceedings of 12th International Conference on Computer Aided Verification","author":"E. M. Clarke","year":"2000","unstructured":"Clarke E M, Grumberg O, Jha S, et al. Counterexamples-guided abstraction refinement. In: Proceedings of 12th International Conference on Computer Aided Verification, LNCS 1855. Berlin: Springer, 2000. 154\u2013169"},{"key":"73_CR3","series-title":"LNCS","first-page":"395","volume-title":"Proceedings of 9th International Static Analysis Symposium","author":"M. M. Gallardo","year":"2002","unstructured":"Gallardo M M, Merino P, Pimentel E. Refinement of LTL formulas for abstract model checking. In: Proceedings of 9th International Static Analysis Symposium, LNCS 2477. Berlin: Springer, 2002. 395\u2013410"},{"key":"73_CR4","volume-title":"Proceedings of 11th International Workshop on Functional and Logic Programming, ENTCS-76","author":"M. M. Gallardo","year":"2002","unstructured":"Gallardo M M, Merino P, Pimentel E. Comparing under-and over-approximations of LTL properties for model checking. In: Proceedings of 11th International Workshop on Functional and Logic Programming, ENTCS-76. Amsterdam: Elsevier, 2002"},{"key":"73_CR5","volume-title":"Proceedings of 7th International Workshop on Formal Methods for Industral Critical Systems, ENTCS-76","author":"M. M. Gallardo","year":"2002","unstructured":"Gallardo M M, Merino P, Pimentel E. A tool for abstraction in model checking. In: Proceedings of 7th International Workshop on Formal Methods for Industral Critical Systems, ENTCS-76. Amsterdam: Elsevier, 2002"},{"issue":"5","key":"73_CR6","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. Model checking and abstraction. ACM Trans Program Lang Syst, 1994, 16(5): 1512\u20131542","journal-title":"ACM Trans Program Lang Syst"},{"key":"73_CR7","series-title":"LNCS","first-page":"184","volume-title":"Proceedings of 6th International SPIN Workshop on Model Checking of Software","author":"M. M. Gallardo","year":"1999","unstructured":"Gallardo M M, Merino P. A framework for automatic construction of abstract promela methods. In: Proceedings of 6th International SPIN Workshop on Model Checking of Software, LNCS 1680. Berlin: Springer, 1999. 184\u2013199"},{"issue":"2","key":"73_CR8","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams D, Gerth R, Grumberg O. Abstract interpretation of reactive systems. ACM Trans Program Lang Syst, 1997, 19(2): 253\u2013291","journal-title":"ACM Trans Program Lang Syst"},{"issue":"1","key":"73_CR9","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/1042038.1042040","volume":"6","author":"Ranzato","year":"2005","unstructured":"Ranzato, Scozzari F. Making abstract domains condensing. ACM Trans Comput Logic, 2005, 6(1): 33\u201360","journal-title":"ACM Trans Comput Logic"},{"issue":"2","key":"73_CR10","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi R, Ranzato F, Scozzari F. Making abstract interpretations complete. J ACM, 2000, 47(2): 361\u2013416","journal-title":"J ACM"},{"key":"73_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-540-31980-1_10","volume-title":"Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Ranzato","year":"2005","unstructured":"Ranzato F, Tapparo F. An abstract interpretation-based refinement algorithm for strong preservation. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3440, Berlin: Springer, 2005. 140\u2013156"},{"issue":"5","key":"73_CR12","first-page":"1","volume":"23","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 1995, 23(5): 1\u201335","journal-title":"Formal Methods in System Design"},{"key":"73_CR13","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/3-540-46017-9_24","volume-title":"Proceedings of 9th International SPIN Workshop on Model Checking of Software","author":"M. M. Gallardo","year":"2002","unstructured":"Gallardo M M, Martinez J, Merino P, et al. \u03b1SPIN: Extending SPIN with Abstraction. In: Proceedings of 9th International SPIN Workshop on Model Checking of Software, LNCS 2318. Berlin: Springer, 2002. 254\u2013258"},{"key":"73_CR14","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G. J. Holzmann","year":"2004","unstructured":"Holzmann G J. The SPIN Model Checker: Primer and Reference Manual. New York: Addison-Wesley, 2004"},{"key":"73_CR15","series-title":"LNCS","first-page":"81","volume-title":"Proceedings of International Symposium on Compositionality","author":"S. Berezin","year":"1997","unstructured":"Berezin S, Campos S, Clarke E M. Compositional reasoning in model checking. In: Proceedings of International Symposium on Compositionality, LNCS 1536. Berlin: Springer, 1997. 81\u2013102"},{"key":"73_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Proceedings of 10th International Conference on Correct Hardware Design and Verification Methods","author":"K. L. McMillan","year":"1999","unstructured":"McMillan K L. Verification of infinite state systems by compositional model checking. In: Proceedings of 10th International Conference on Correct Hardware Design and Verification Methods, LNCS 1703. Berlin: Springer, 1999. 219\u2013234"},{"key":"73_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-540-30476-0_8","volume-title":"Proceedings of 2th International Symposium on Automated Technology on Verification and Analysis (ATVA\u201904)","author":"B. Su","year":"2004","unstructured":"Su B, Zhang W. Search space partition and case basis exploration for reducing model checking complexity. In: Proceedings of 2th International Symposium on Automated Technology on Verification and Analysis (ATVA\u201904), LNCS 3299. Berlin: Springer, 2004. 34\u201348"},{"issue":"6","key":"73_CR18","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1007\/BF02945465","volume":"18","author":"W. Zhang","year":"2003","unstructured":"Zhang W. Combining static analysis and case-based search space partition for reducing peek memory in model checking. J Comput Sci Tech, 2003, 18(6): 762\u2013770","journal-title":"J Comput Sci Tech"},{"key":"73_CR19","series-title":"LNCS","first-page":"190","volume-title":"Proceedings of 2th International Workshop on Rapid Intergration of Software Engineering Techniques","author":"F. Pu","year":"2005","unstructured":"Pu F, Zhang W, Wang S. An improved cased-based approach to LTL model checking. In: Proceedings of 2th International Workshop on Rapid Intergration of Software Engineering Techniques, LNCS 3943. Berlin: Springer, 2005. 190\u2013202"},{"key":"73_CR20","series-title":"LNCS","first-page":"200","volume-title":"Proceedings of 6th International SPIN Workshop on Model Checking of Software","author":"W. Zhang","year":"1999","unstructured":"Zhang W. Model checking operator procedures. In: Proceedings of 6th International SPIN Workshop on Model Checking of Software, LNCS 1680. Berlin: Springer, 1999, 200\u2013215"},{"issue":"4","key":"73_CR21","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s100090050041","volume":"2","author":"L. I. Milett","year":"2002","unstructured":"Milett L I, Teitelbaum T. Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation. Int J Software Tools for Tech Trans, 2002, 2(4): 343\u2013349","journal-title":"Int J Software Tools for Tech Trans"},{"issue":"11","key":"73_CR22","doi-asserted-by":"crossref","first-page":"1325","DOI":"10.1109\/TC.2006.170","volume":"55","author":"Q. Wu","year":"2006","unstructured":"Wu Q, Hsiao M S. A new simulation-based property checking algorithm based on partitioned alternative search space traversal. IEEE Trans Comput, 2006, 55(11): 1325\u20131334","journal-title":"IEEE Trans Comput"},{"key":"73_CR23","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-47813-2_21","volume-title":"Proceedings of 12th International Conference on Verification, Model Checking and Abstract Interpretation","author":"M. Huth","year":"2002","unstructured":"Huth M. Model checking modal transition systems using Kripke structures. In: Proceedings of 12th International Conference on Verification, Model Checking and Abstract Interpretation, LNCS 2294. Berlin: Springer, 2002, 302\u2013316"},{"key":"73_CR24","series-title":"LNCS","first-page":"155","volume-title":"Proceedings of European Symposium On Programming","author":"M. Huth","year":"2001","unstructured":"Huth M, Jagadeesan R, Schmit D. Modal transition syatems: A foundation for three-valued program analysis. In: Proceedings of European Symposium On Programming, LNCS 2028. Berlin: Springer, 2001. 155\u2013169"}],"container-title":["Science in China Series F: Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0073-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-007-0073-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0073-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T15:35:54Z","timestamp":1559403354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-007-0073-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":24,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["73"],"URL":"https:\/\/doi.org\/10.1007\/s11432-007-0073-y","relation":{},"ISSN":["1009-2757","1862-2836"],"issn-type":[{"value":"1009-2757","type":"print"},{"value":"1862-2836","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}