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