{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:23Z","timestamp":1725573083975},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_17","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"250-266","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking of Systems Employing Commutative Functions"],"prefix":"10.1007","author":[{"given":"A. Prasad","family":"Sistla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaodong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajmani, S.K.: The slam toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 260. Springer, Heidelberg (2001)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bouyer, E., Fleury, P., Larsen, K.G.: Static guard analysis in timed automata verification. In: TACAS, pp. 254\u2013270 (2003)","DOI":"10.1007\/3-540-36577-X_18"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with, periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 55\u201367. Springer, Heidelberg (1994)"},{"issue":"4","key":"17_CR4","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1909","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Trans. Program. Lang. Syst.\u00a021(4), 747\u2013789 (1909)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counter-example guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem","author":"C.P. Godefroid","year":"1996","unstructured":"Godefroid, C.P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/129712.129738","volume-title":"Proceedings of the tuienty-fourth annual ACM symposium on Theory of computing","author":"D. Lee","year":"1992","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: Proceedings of the tuienty-fourth annual ACM symposium on Theory of computing, pp. 264\u2013274. ACM Press, New York (1992)"},{"key":"17_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: CAV 2000, pp. 435\u2013449 (2000)","DOI":"10.1007\/10722167_33"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all, on model-checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and model check while yon prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/350887.350891","volume":"9","author":"A.P. Sistla","year":"2000","unstructured":"Sistla, A.P., Gyuris, V., Emerson, E.A.: SMC: A symmetry based model checker for safety and liveness properties. ACM Transactions on. Software Engineering Methodologies\u00a09(2), 133\u2013166 (2000)","journal-title":"ACM Transactions on. Software Engineering Methodologies"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:31:23Z","timestamp":1620012683000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}