@article(AEI09,
 author       = {M.~Alpuente and S.~Escobar and J.~Iborra},
 year         = {2009},
 title        = {{Termination of Narrowing Revisited}},
 journal      = {Theoretical Computer Science},
 volume       = {410},
 number       = {46},
 pages        = {4608--4625},
 doi          = {10.1016/j.tcs.2009.07.037},
)
@article(AEI11,
 author       = {M.~Alpuente and S.~Escobar and J.~Iborra},
 year         = {2011},
 title        = {{Modular Termination of Basic Narrowing and Equational Unification}},
 journal      = {{Logic Journal of the IGPL}},
 volume       = {19},
 number       = {6},
 pages        = {731--762},
 doi          = {10.1007/978-3-540-70590-1\_1},
)
@incollection(BS-handbook00,
 author       = {F.~Baader and W.~Snyder},
 year         = {2001},
 title        = {{Unification Theory}},
 editor       = {J.~A. Robinson and A.~Voronkov},
 booktitle    = {{Handbook of Automated Reasoning}},
 volume       = {I},
 publisher    = {{Elsevier Science}},
 pages        = {447--533},
 doi          = {10.1016/B978-044450813-3/50010-2},
)
@inproceedings(BEM13,
 author       = {K.~Bae and S.~Escobar and J.~Meseguer},
 year         = {2013},
 title        = {{Abstract Logical Model Checking of Infinite-State Systems Using Narrowing}},
 booktitle    = {{Proc. of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013)}},
 series       = {{LIPIcs}},
 volume       = {21},
 publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik}},
 pages        = {81--96},
 doi          = {10.4230/LIPIcs.RTA.2013.81},
)
@inproceedings(BGLN13,
 author       = {C.~Bouchard and K.~A. Gero and C.~Lynch and P.~Narendran},
 year         = {2013},
 title        = {{On Forward Closure and the Finite Variant Property}},
 booktitle    = {{Proc. of the 9th International Symposium on Frontiers of Combining Systems (FroCos 2013)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8152},
 publisher    = {{Springer}},
 pages        = {327--342},
 doi          = {10.1007/978-3-642-40885-4\_23},
)
@techreport(CME14tr,
 author       = {A.~Cholewa and J.~Meseguer and S.~Escobar},
 year         = {2014},
 title        = {{Variants of Variants and the Finite Variant Property}},
 type         = {Technical Report},
 institution  = {{University of Illinois at Urbana-Champaign}},
 url          = {http://hdl.handle.net/2142/47117},
)
@techreport(maude-manual,
 author       = {M.~Clavel and F.~Dur{\'a}n and S.~Eker and S.~Escobar and P.~Lincoln and N.~Mart{\'i}-Oliet and J.~Meseguer and C.~Talcott},
 year         = {2016},
 title        = {{Maude Manual (Version 2.7.1)}},
 type         = {Technical Report},
 institution  = {{SRI International Computer Science Laboratory}},
 note         = {Available at: \url{http://maude.cs.uiuc.edu/maude2-manual/}},
)
@book(Maude07,
 author       = {M.~Clavel and F.~Dur{\'a}n and S.~Eker and P.~Lincoln and N.~Mart{\'i}-Oliet and J.~Meseguer and C.~Talcott},
 year         = {2007},
 title        = {{All About Maude: A High-Performance Logical Framework}},
 publisher    = {{Springer}},
 doi          = {10.1007/978-3-540-71999-1},
)
@inproceedings(CD05,
 author       = {H.~Comon-Lundh and S.~Delaune},
 year         = {2005},
 title        = {{The Finite Variant Property: How to Get Rid of Some Algebraic Properties}},
 booktitle    = {{Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {3467},
 publisher    = {{Springer}},
 pages        = {294--307},
 doi          = {10.1007/978-3-540-32033-3\_22},
)
@inproceedings(DDKS17,
 author       = {J.~Dreier and C.~Dum{\'{e}}nil and S.~Kremer and R.~Sasse},
 year         = {2017},
 title        = {{Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols}},
 booktitle    = {{Proc. of the 6th International Symposium on Principles of Security and Trust (POST 2017)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10204},
 publisher    = {{Springer}},
 pages        = {117--140},
 doi          = {10.1007/978-3-662-54455-6\_6},
)
@inproceedings(DHRS18,
 author       = {J.~Dreier and L.~Hirschi and S.~Radomirovic and R.~Sasse},
 year         = {2018},
 title        = {{Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR}},
 booktitle    = {{Proc. of the 31st International Symposium on Computer Security Foundations (CSF 2015)}},
 publisher    = {{IEEE Computer Society Press}},
 pages        = {359--373},
 doi          = {10.1109/CSF.2018.00033},
)
@inproceedings(DEEM+18,
 author       = {F.~Dur{\'a}n and S.~Eker and S.~Escobar and N.~Mart{\'i}-Oliet and J.~Meseguer and C.~Talcott},
 year         = {2018},
 title        = {{Associative Unification and Symbolic Reasoning Modulo Associativity in Maude}},
 booktitle    = {{Proc. of the 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11152},
 publisher    = {{Springer}},
 pages        = {98--114},
 doi          = {10.1016/j.scico.2014.02.005},
)
@inproceedings(DLM09,
 author       = {F.~Dur{\'a}n and S.~Lucas and J.~Meseguer},
 year         = {2009},
 title        = {{Termination Modulo Combinations of Equational Theories}},
 booktitle    = {{Proc. of the 7th International Symposium on Frontiers of Combining Systems (FroCos 2009)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {5749},
 publisher    = {{Springer}},
 pages        = {246--262},
 doi          = {10.1007/978-3-642-04222-5\_15},
)
@article(DM12,
 author       = {F.~Dur{\'{a}n} and J.~Meseguer},
 year         = {2012},
 title        = {{On the Church-Rosser and Coherence Properties of Conditional Order-sorted Rewrite Theories}},
 journal      = {The Journal of Logic and Algebraic Programming},
 volume       = {81},
 number       = {7--8},
 pages        = {816--850},
 doi          = {10.1016/j.jlap.2011.12.004},
)
@inproceedings(EEMR19,
 author       = {A.~K. Eeralla and S.~Erbatur and A.~M. Marshal and C.~Ringeissen},
 year         = {2019},
 title        = {{Rule-based Unification in Combined Theories and the Finite Variant Property}},
 booktitle    = {{Proc. of the 13th International Conference on Language and Automata Theory and Applications (LATA 2019)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11417},
 publisher    = {{Springer}},
 pages        = {356--367},
 doi          = {10.1007/978-3-030-13435-8\_26},
)
@inproceedings(EKMN+15,
 author       = {S.~Erbatur and D.~Kapur and A.~M. Marshall and P.~Narendran and C.~Ringeissen},
 year         = {2015},
 title        = {{Unification and Matching in Hierarchical Combinations of Syntactic Theories}},
 booktitle    = {{Proc. of the 10th International Symposium on Frontiers of Combining Systems (FroCos 2015)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9322},
 publisher    = {{Springer}},
 pages        = {291--306},
 doi          = {10.1007/978-3-319-24246-0\_18},
)
@inproceedings(EMM09,
 author       = {S.~Escobar and C.~Meadows and J.~Meseguer},
 year         = {2009},
 title        = {{Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties}},
 booktitle    = {{Foundations of Security Analysis and Design V (FOSAD 2007/2008/2009 Tutorial Lectures)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {5705},
 publisher    = {{Springer}},
 pages        = {1--50},
 doi          = {10.1007/978-3-642-03829-7\_1},
)
@inproceedings(EM07,
 author       = {S.~Escobar and J.~Meseguer},
 year         = {2007},
 title        = {{Symbolic Model Checking of Infinite-State Systems Using Narrowing}},
 booktitle    = {{Proc. of the 18th International Conference on Term Rewriting and Applications (RTA 2007)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4533},
 publisher    = {{Springer}},
 pages        = {153--168},
 doi          = {10.1007/978-3-540-73449-9\_13},
)
@article(ESM12,
 author       = {S.~Escobar and R.~Sasse and J.~Meseguer},
 year         = {2012},
 title        = {{Folding Variant Narrowing and Optimal Variant Termination}},
 journal      = {The Journal of Logic and Algebraic Programming},
 volume       = {81},
 number       = {7--8},
 pages        = {898--928},
 doi          = {10.1016/j.jlap.2012.01.002},
)
@misc(full-maude,
 year         = {2019},
 title        = {{Full Maude Website}},
 note         = {{Available at: \url{https://github.com/maude-team/full-maude}}},
)
@phdthesis(Hullot80,
 author       = {J.~M. Hullot},
 year         = {1980},
 title        = {{Compilation de Formes Canoniques dans les Th\'eories Equationnelles}},
 school       = {{Universit{\'e} de Paris-Sud}},
)
@inproceedings(JKK83,
 author       = {J.~P. Jouannaud and C.~Kirchner and H.~Kirchner},
 year         = {1983},
 title        = {{Incremental Construction of Unification Algorithms in Equational Theories}},
 booktitle    = {{Proc. of the 17th International Colloquium on Automata, Languages and Programming (ICALP 1990)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {154},
 publisher    = {{Springer}},
 pages        = {361--373},
 doi          = {10.1007/BFb0036921},
)
@article(JK86,
 author       = {J.~P. Jouannaud and H.~Kirchner},
 year         = {1986},
 title        = {{Completion of a Set of Rules Modulo a Set of Equations}},
 journal      = {{SIAM Journal on Computing}},
 volume       = {15},
 number       = {4},
 pages        = {1155--1194},
 doi          = {10.1137/0215084},
)
@article(KN87,
 author       = {D.~Kapur and P.~Narendran},
 year         = {1987},
 title        = {{Matching, Unification and Complexity}},
 journal      = {{ACM SIGSAM Bulletin}},
 volume       = {21},
 number       = {4},
 pages        = {6--9},
 doi          = {10.1145/36330.36332},
)
@article(LM16,
 author       = {S.~Lucas and J.~Meseguer},
 year         = {2016},
 title        = {{Normal Forms and Normal Theories in Conditional Rewriting}},
 journal      = {Journal of Logical and Algebraic Methods in Programming},
 volume       = {85},
 pages        = {67--97},
 doi          = {10.1016/j.jlamp.2015.06.001},
)
@inproceedings(MSCB13,
 author       = {S.~Meier and B.~Schmidt and C.~Cremers and D.~A. Basin},
 year         = {2013},
 title        = {{The TAMARIN Prover for the Symbolic Analysis of Security Protocols}},
 booktitle    = {{Proc. of the 25th International Conference on Computer Aided Verification (CAV 2013)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {{Springer}},
 pages        = {696--701},
 doi          = {10.1007/978-3-642-39799-8\_48},
)
@article(Meseguer92,
 author       = {J.~Meseguer},
 year         = {1992},
 title        = {{Conditional Rewriting Logic as a United Model of Concurrency}},
 journal      = {Theoretical Computer Science},
 volume       = {96},
 number       = {1},
 pages        = {73--155},
 doi          = {10.1016/0304-3975(92)90182-F},
)
@inproceedings(Meseguer97,
 author       = {J.~Meseguer},
 year         = {1997},
 title        = {{Membership Algebra as a Logical Framework for Equational Specification}},
 booktitle    = {{Proc. of the 12th International Workshop on Algebraic Development Techniques (WADT 1997)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {1376},
 publisher    = {{Springer}},
 pages        = {18--61},
 doi          = {10.1007/3-540-64299-4\_26},
)
@article(Meseguer12,
 author       = {J.~Meseguer},
 year         = {2012},
 title        = {{Twenty Years of Rewriting Logic}},
 journal      = {The Journal of Logic and Algebraic Programming},
 volume       = {81},
 number       = {7-8},
 pages        = {721--781},
 doi          = {10.1016/j.jlap.2012.06.003},
)
@article(Meseguer17,
 author       = {J.~Meseguer},
 year         = {2017},
 title        = {{Strict Coherence of Conditional Rewriting Modulo Axioms}},
 journal      = {Theoretical Computer Science},
 volume       = {672},
 pages        = {1--35},
 doi          = {10.1016/j.tcs.2016.12.026},
)
@inproceedings(Meseguer18-wollic,
 author       = {J.~Meseguer},
 year         = {2018},
 title        = {{Symbolic Reasoning Methods in Rewriting Logic and Maude}},
 booktitle    = {{Proc. of the 25th International Workshop on Logic, Language, Information, and Computation (WoLLIC 2018)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10944},
 publisher    = {{Springer}},
 pages        = {25--60},
 doi          = {10.1007/978-3-662-57669-4\_2},
)
@article(Meseguer18-scp,
 author       = {J.~Meseguer},
 year         = {2018},
 title        = {{Variant-based Satisfiability in Initial Algebras}},
 journal      = {Science of Computer Programming},
 volume       = {154},
 pages        = {3--41},
 doi          = {10.1016/j.scico.2017.09.001},
)
@inproceedings(Riesco14,
 author       = {A.~Riesco},
 year         = {2014},
 title        = {{Using Big-Step and Small-Step Semantics in {M}aude to Perform Declarative Debugging}},
 booktitle    = {{Proc. of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8475},
 publisher    = {{Springer}},
 pages        = {52--68},
 doi          = {10.1007/978-3-319-07151-0\_4},
)
@inproceedings(Rusu10,
 author       = {V.~Rusu},
 year         = {2010},
 title        = {{Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications}},
 booktitle    = {{Proc. of the 4th International Conference on Tests and Proofs (TAP 2010)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6143},
 publisher    = {{Springer}},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-13977-2\_12},
)
@book(Terese03,
 author       = {TeReSe},
 year         = {2003},
 title        = {{Term Rewriting Systems}},
 publisher    = {{Cambridge University Press}},
 doi          = {10.1017/S095679680400526X},
)
@article(TGRK15,
 author       = {E.~Tushkanova and A.~Giorgetti and C.~Ringeissen and O.~Kouchnarenko},
 year         = {2015},
 title        = {{A Rule-based System for Automatic Decidability and Combinability}},
 journal      = {Science of Computer Programming},
 volume       = {99},
 pages        = {3--23},
 doi          = {10.1016/j.scico.2014.02.005},
)