{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:30Z","timestamp":1725574590245},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236108"},{"type":"electronic","value":"9783540304760"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30476-0_8","type":"book-chapter","created":{"date-parts":[[2011,1,12]],"date-time":"2011-01-12T17:51:35Z","timestamp":1294854695000},"page":"34-48","source":"Crossref","is-referenced-by-count":4,"title":["Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity"],"prefix":"10.1007","author":[{"given":"Bai","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-49213-5_4","volume-title":"Compositionality: The Significant Difference","author":"S. Berezin","year":"1998","unstructured":"Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 81\u2013102. Springer, Heidelberg (1998)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science B, 997\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"8_CR3","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"8_CR4","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":"5","key":"8_CR5","doi-asserted-by":"publisher","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 Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Proceedings of the 2nd International Workshop on Tools and Algorithms for the construction and Analysis of Systems","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"10","key":"8_CR7","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G. Lowe","year":"1997","unstructured":"Lowe, G., Roscoe, A.W.: Using CSP to Detect Errors in the TMN Protocol. IEEE Trans. Software Eng.\u00a023(10), 659\u2013669 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"8_CR8","volume-title":"Lex & Yacc","author":"T. Mason","year":"1992","unstructured":"Mason, T., Levine, J., Brown, D.: Lex & Yacc, 2nd edn. O\u2019Reilly and Associates, California (1992)","edition":"2"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"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: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013234. Springer, Heidelberg (1999)"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","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\u00a02(4), 343\u2013349 (2000)","journal-title":"STTT"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-46017-9_14","volume-title":"Model Checking Software","author":"P. Maggi","year":"2002","unstructured":"Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 187\u2013204. Springer, Heidelberg (2002)"},{"issue":"3","key":"8_CR12","first-page":"254","volume":"19","author":"H.-B. Sun","year":"2002","unstructured":"Sun, H.-B., Lin, D.-D.: An improvement of the TMN protocol based on trapdoor oneway functions. Journal of the Graduate School of the Chinese Academy of Sciences\u00a019(3), 254\u2013262 (2002)","journal-title":"Journal of the Graduate School of the Chinese Academy of Sciences"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-48234-2_16","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"W. Zhang","year":"1999","unstructured":"Zhang, W.: Model checking operator procedures. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 200\u2013215. Springer, Heidelberg (1999)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-40891-6_5","volume-title":"Computer Safety, Reliability, and Security","author":"W. Zhang","year":"2000","unstructured":"Zhang, W.: Validation of control system specifications with abstract plant models. In: Koornneef, F., van der Meulen, M.J.P. (eds.) SAFECOMP 2000. LNCS, vol.\u00a01943, pp. 53\u201362. Springer, Heidelberg (2000)"},{"issue":"6","key":"8_CR15","doi-asserted-by":"publisher","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 Partitioning for Reducing Peak Memory in Model Checking. Journal of Computer Science and Technology\u00a018(6), 762\u2013770 (2003)","journal-title":"Journal of Computer Science and Technology"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30476-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:02:46Z","timestamp":1620014566000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30476-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236108","9783540304760"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30476-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}