{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:11Z","timestamp":1725551951598},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_25","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"381-397","source":"Crossref","is-referenced-by-count":13,"title":["Systematic Construction of Abstractions for Model-Checking"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[]},{"given":"Ou","family":"Wei","sequence":"additional","affiliation":[]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-24730-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Levin, V., Xie, F.: Automatic Creation of Environment Models via Training. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 93\u2013107. Springer, Heidelberg (2004)"},{"key":"25_CR2","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., Rajamani, S.: \u201cThe SLAM Toolkit\u201d. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Belnap, N.D.: A Useful Four-Valued Logic. In: Dunn, Epstein (eds.) Modern Uses of Multiple-Valued Logic, Reidel, pp. 30\u201356 (1977)","DOI":"10.1007\/978-94-010-1161-7_2"},{"issue":"4","key":"25_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/990010.990011","volume":"12","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM TOSEM\u00a012(4), 1\u201338 (2003)","journal-title":"ACM TOSEM"},{"issue":"5","key":"25_CR5","doi-asserted-by":"publisher","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 TOPLAS\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM TOPLAS"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: ICSE 2000, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"4","key":"25_CR7","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"19","key":"25_CR8","doi-asserted-by":"crossref","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":"25_CR9","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-24730-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: \u201cModel Checking Discounted Temporal Properties\u201d. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 77\u201392. Springer, Heidelberg (2004)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-Valued Abstractions of Games: Uncertainty, but with Precision. In: LICS 2004, pp. 170\u2013179 (2004)","DOI":"10.1109\/LICS.2004.1319611"},{"issue":"1-2","key":"25_CR12","first-page":"105","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. FMSD\u00a09(1-2), 105\u2013131 (1996)","journal-title":"FMSD"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Wahl, T.: Dynamic Symmetry Reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 382\u2013396. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31980-1_25"},{"key":"25_CR14","unstructured":"Fitting, M.: Bilattices are Nice Things. In: Conference on Self-Reference (2002)"},{"issue":"3","key":"25_CR15","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1111\/j.1467-8640.1988.tb00280.x","volume":"4","author":"M.L. Ginsberg","year":"1988","unstructured":"Ginsberg, M.L.: Multivalued Logics: A Uniform Approach to Reasoning in Artificial Intelligence. Computational Intelligence\u00a04(3), 265\u2013316 (1988)","journal-title":"Computational Intelligence"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44685-0_29"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"25_CR18","unstructured":"Gurfinkel, A., Chechik, M.: Yasm: Model-Checking Software with Belnap Logic. Technical Report 533, University of Toronto (April 2005)"},{"key":"25_CR19","unstructured":"Gurfinkel: A., Wei, O., Chechik, M.: Logical Abstract Interpretation. Technical Report 532, University of Toronto (September 2005)"},{"key":"25_CR20","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the Propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 334\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: LICS 1988, pp. 203\u2013210 (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property Preserving Abstractions for the Verification of Concurrent Systems. FMSD\u00a06, 1\u201335 (1995)","DOI":"10.1007\/BF01384313"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Closed and Logical Relations for Over- and Under-Approximation of Powersets. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 22\u201337. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-27864-1_5"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Shoham, S., Grumberg, O.: Monotonic Abstraction-Refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 546\u2013560. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24730-2_40"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/11560548_22","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Wei","year":"2005","unstructured":"Wei, O., Gurfinkel, A., Chechik, M.: Identification and Counter Abstraction for Full Virtual Symmetry. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 285\u2013300. Springer, Heidelberg (2005)"}],"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\/11609773_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:04Z","timestamp":1619507224000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11609773_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}