{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:12Z","timestamp":1762459392255},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_13","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"183-192","source":"Crossref","is-referenced-by-count":9,"title":["Built-in Variant Generation and Unification, and Their Applications in Maude 2.7"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Eker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"13_CR1","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F., (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24\u201326, 2013, Eindhoven, The Netherlands. LIPIcs vol. 21, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/978-3-642-40885-4_23","volume-title":"Frontiers of Combining Systems","author":"C Bouchard","year":"2013","unstructured":"Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 327\u2013342. Springer, Heidelberg (2013)"},{"key":"13_CR3","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, University of Illinois at Urbana-Champaign (2014). http:\/\/hdl.handle.net\/2142\/47117"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-642-02348-4_27","volume-title":"Rewriting Techniques and Applications","author":"M Clavel","year":"2009","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Unification and narrowing in maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 380\u2013390. Springer, Heidelberg (2009)"},{"key":"13_CR5","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. 4350. Springer, Heidelberg (2007)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 3467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"13_CR7","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Meseguer, J., Talcott, C.L.: Variants, unification, narrowing, and symbolic reachability inMaude 2.6. In: Schmidt-Schau\u00df, M., (ed.) Proceedings of the 22ndInternational Conference on Rewriting Techniques and Applications, RTA2011, May 30 - June 1, 2011, Novi Sad, Serbia. LIPIcs, vol. 10, pp. 31\u201340. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"Frontiers of Combining Systems","author":"F Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246\u2013262. Springer, Heidelberg (2009)"},{"issue":"7\u20138","key":"13_CR9","doi-asserted-by":"crossref","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Logic Algebraic Program. 81(7\u20138), 816\u2013850 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2007","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equationalproperties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2007)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"issue":"7\u20138","key":"13_CR12","doi-asserted-by":"crossref","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. Logic Algebraic Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"computer aided verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"13_CR14","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Technical report, University of Illinois at Urbana-Champaign (2015). http:\/\/hdl.handle.net\/2142\/88408"},{"issue":"1\u20132","key":"13_CR15","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High. Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"High. Order Symbolic Comput."},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-319-07151-0_4","volume-title":"functional and logic programming","author":"A Riesco","year":"2014","unstructured":"Riesco, A.: Using big-step and small-step semantics in maude to perform declarative debugging. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 52\u201368. Springer, Heidelberg (2014)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-642-13977-2_12","volume-title":"Tests and Proofs","author":"V Rusu","year":"2010","unstructured":"Rusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 135\u2013150. Springer, Heidelberg (2010)"},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2014.02.005","volume":"99","author":"E Tushkanova","year":"2015","unstructured":"Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. Sci. Comput. Program. 99, 3\u201323 (2015)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:12:43Z","timestamp":1498306363000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}