{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:55Z","timestamp":1761597235195},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_2","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"2-16","source":"Crossref","is-referenced-by-count":22,"title":["Equational Abstractions"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miguel","family":"Palomino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-49059-0_15","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"P. Abdulla","year":"1999","unstructured":"Abdulla, P., Annichini, A., Bouajjani, A.: Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 208. Springer, Heidelberg (1999)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"2_CR3","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 Transactions on Programming Languages and Systems\u00a016, 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"2_CR5","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.M. Clarke","year":"2000","unstructured":"Clarke, E.M., 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":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"1998","unstructured":"Col\u00f3n, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems\u00a019, 253\u2013291 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 662\u2013681. Springer, Heidelberg (1996)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. International Journal on Software Tools for Technology Transfer\u00a04, 328\u2013342 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmentary finitary abstraction. Information and Computation\u00a0163, 203\u2013243 (2000)","journal-title":"Information and Computation"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06, 1\u201336 (1995)","journal-title":"Formal Methods in System Design"},{"key":"2_CR12","unstructured":"Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, Univ. of Texas at Austin (2001)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60580-0","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. M\u00fcller","year":"1995","unstructured":"M\u00fcller, O., Nipkow, T.: Combining model checking and deduction for I\/Oautomata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 1\u201316. Springer, Heidelberg (1995)"},{"key":"2_CR14","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. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"2_CR15","unstructured":"Uribe Restrepo, T.E.: Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Dept. of Computer Science, Stanford Univ. (1998)"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Ecker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science\u00a0285, 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"2_CR17","series-title":"ENTCS","volume-title":"Rewriting Logic and its Applications, WRLA 2004","author":"S. Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Rewriting Logic and its Applications, WRLA 2004. ENTCS, vol.\u00a071. Elsevier, Amsterdam (2002)"},{"key":"2_CR18","unstructured":"Clavel, M.: The ITP tool. In: Nepomuceno, A., et al. (eds.) Logic, Language, and Information, Kronos, pp. 55\u201362 (2001)"},{"key":"2_CR19","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser checker tool for Maude equational specifications (2000), http:\/\/maude.cs.uiuc.edu\/tools"},{"key":"2_CR20","unstructured":"Dur\u00e1n, F.: Coherence checker and completion tools for Maude specifications (2000), http:\/\/maude.cs.uiuc.edu\/tools"},{"key":"2_CR21","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Notes on model checking and abstraction in rewriting logic (2002), http:\/\/formal.cs.uiuc.edu\/texts\/nmcarl.ps"},{"key":"2_CR22","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. Theoretical Computer Science\u00a096, 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"285","author":"P. Borovansk\u00fd","year":"2002","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Moreau, P.E.: ELAN from a rewriting logic point of view. Theoretical Computer Science\u00a0285, 155\u2013185 (2002)","journal-title":"Theoretical Computer Science"},{"key":"2_CR25","volume-title":"CafeOBJ Report","author":"K. Futatsugi","year":"1998","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)"},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Communications of the ACM\u00a017, 453\u2013455 (1974)","journal-title":"Communications of the ACM"},{"key":"2_CR27","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science\u00a0285 (2002)","DOI":"10.1016\/S0304-3975(01)00366-8"},{"key":"2_CR29","unstructured":"Contejean, E., March\u00e9, C.: The CiME system: tutorial and user\u2019s manual. Manuscript, Univ. Paris-Sud, Centre d\u2019Orsay"},{"key":"2_CR30","unstructured":"Dur\u00e1n, F.: Termination checker and Knuth-Bendix completion tools for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http:\/\/maude.cs.uiuc.edu\/papers"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,13]],"date-time":"2020-06-13T09:16:39Z","timestamp":1592039799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}