{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:03:01Z","timestamp":1768266181487,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319089171","type":"print"},{"value":"9783319089188","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_5","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T01:44:22Z","timestamp":1404265462000},"page":"61-76","source":"Crossref","is-referenced-by-count":11,"title":["Predicate Abstraction of Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-15375-4_7","volume-title":"CONCUR 2010 - Concurrency Theory","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Delzanno, G., Haziza, F., Hong, C.-D., Rezine, A.: Constrained monotonic abstraction: A CEGAR for parameterized verification. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 86\u2013101. Springer, Heidelberg (2010)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-58216-9_40","volume-title":"Logic Programming and Automated Reasoning","author":"J. Avenhaus","year":"1994","unstructured":"Avenhaus, J., Lor\u00eda-S\u00e1enz, C.: On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 215\u2013229. Springer, Heidelberg (1994)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"5_CR4","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA. LIPIcs, vol.\u00a021, pp. 81\u201396 (2013)"},{"issue":"5","key":"5_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. ACM SIGPLAN Notices\u00a036(5), 203\u2013213 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H. Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013320. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S. Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic and Logic Programming\u00a081, 898\u2013928 (2012)","journal-title":"J. Algebraic and Logic Programming"},{"issue":"5","key":"5_CR15","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1016\/j.jsc.2010.01.009","volume":"45","author":"T. Genet","year":"2010","unstructured":"Genet, T., Rusu, V.: Equational approximations for tree automata completion. Journal of Symbolic Computation\u00a045(5), 574\u2013597 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","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)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"issue":"1","key":"5_CR19","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comp. Sci.\u00a096(1), 73\u2013155 (1992)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J. Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic and Logic Programming\u00a081, 721\u2013781 (2012)","journal-title":"J. Algebraic and Logic Programming"},{"issue":"2-3","key":"5_CR21","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J. Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. Theor. Comp. Sci.\u00a0403(2-3), 239\u2013264 (2008)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-44881-0_34","volume-title":"Rewriting Techniques and Applications","author":"H. Ohsaki","year":"2003","unstructured":"Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed A-tree languages with membership conditional rewriting mechanism. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 483\u2013498. Springer, Heidelberg (2003)"},{"key":"5_CR23","unstructured":"Palomino, M.: A predicate abstraction tool for maude (2005), http:\/\/maude.sip.ucm.es\/~miguelpt\/bibliography.html"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comp. Sci.\u00a0285 (2002)","DOI":"10.1016\/S0304-3975(01)00366-8"},{"issue":"2","key":"5_CR25","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,10]],"date-time":"2022-04-10T04:55:07Z","timestamp":1649566507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}