{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T20:10:04Z","timestamp":1736021404633,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_22","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"285-300","source":"Crossref","is-referenced-by-count":7,"title":["Identification and Counter Abstraction for Full Virtual Symmetry"],"prefix":"10.1007","author":[{"given":"Ou","family":"Wei","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A Backtrack Search Pseudo-Boolean Solver. In: SAT 2002, pp. 346\u2013353 (2002)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45657-0_8","volume-title":"Computer Aided Verification","author":"S. Barner","year":"2002","unstructured":"Barner, S., Grumberg, O.: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 93\u2013106. Springer, Heidelberg (2002)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"22_CR5","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1982)"},{"issue":"1-2","key":"22_CR7","first-page":"77","volume":"9","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. FMSD\u00a09(1-2), 77\u2013104 (1996)","journal-title":"FMSD"},{"issue":"19","key":"22_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"2","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM TOPLAS\u00a02(19), 253\u2013291 (1997)","journal-title":"ACM TOPLAS"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E., Havlicek, J., Trefler, R.: Virtual Symmetry Reduction. In: LICS 2000, pp. 121\u2013131 (2000)","DOI":"10.1109\/LICS.2000.855761"},{"issue":"1-2","key":"22_CR10","first-page":"105","volume":"9","author":"E. Emerson","year":"1996","unstructured":"Emerson, E., Sistla, A.: Symmetry and Model Checking. FMSD\u00a09(1-2), 105\u2013131 (1996)","journal-title":"FMSD"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Emerson","year":"1999","unstructured":"Emerson, E., Trefler, R.: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 142\u2013157. Springer, Heidelberg (1999)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-39724-3_20","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Emerson","year":"2003","unstructured":"Emerson, E., Wahl, T.: On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 216\u2013230. Springer, Heidelberg (2003)"},{"issue":"1-2","key":"22_CR13","first-page":"41","volume":"9","author":"C. Ip","year":"1996","unstructured":"Ip, C., Dill, D.: Better Verification Through Symmetry. FMSD\u00a09(1-2), 41\u201375 (1996)","journal-title":"FMSD"},{"issue":"4","key":"22_CR14","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.: On the Complexity of Integer Programming. J. ACM\u00a028(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, \u221e)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Comm. of the ACM (August 1992)","DOI":"10.1145\/125826.125848"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: An Automata-Theoretic Approach to Presburger Arithmetic Constraints. In: SAS 1995. LNCS, vol.\u00a01785, pp. 21\u201332 (1995)","DOI":"10.1007\/3-540-60360-3_30"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T19:51:42Z","timestamp":1736020302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11560548_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}