Publications - Variant Narrowing & Narrowing in Maude

2025

Raúl López-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar, and Kazuhiro Ogata.
Folding Variant Narrowing for the Analysis of Mutual Exclusion Protocols.
In proceedings of 27th International Symposium on Principles and Practice of Declarative Programming (PPDP 2025). To appear 2025
© ACM Press

2024

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, Jose Meseguer, Rubén Rubio, and Carolyn Talcott.
Programming Open Distributed Systems in Maude.
In proceedings of 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024).
© ACM Press
Available: DOI

Francisco Durán, Santiago Escobar, Jose Meseguer, and Julia Sapiña.
NuITP: An Inductive Theorem Prover for Equational Program Verification.
In proceedings of 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024).
© ACM Press
Available: DOI

Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, Jose Meseguer, Julia Sapiña.
Verifying Invariants by Deductive Model Checking.
In Kazuhiro Ogata (ed), 15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024.
Lecture Notes in Computer Science, volume 14953, pages 3-21.
© Springer-Verlag
Available: DOI

Santiago Escobar, Narciso Martí-Oliet, Rubén Rubio.
Towards a strategy language for narrowing in Maude.
In Kazuhiro Ogata (ed), 15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024.

2023

Santiago Escobar, Raul López, Julia Sapiña.
Symbolic analysis by using folding narrowing with irreducibility and SMT constraints.
In Proceedings of 9th ACM International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023), Cascais, Portugal, October 22, 2023.
© ACM Press

Raúl López, Santiago Escobar, Julia Sapiña
An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis.
Journal of Logical and Algebraic Methods in Programming, July 2023. In Press
© Elsevier Science
Available: DOI

Santiago Escobar
Extensions of Logic Programming in Maude
Feature Article of Association for Logic Programming. February 2023
Available: Online

2022

Raúl López-Rueda, Santiago Escobar.
Canonical Narrowing for Variant-based Conditional Rewrite Theories.
In Adrián Riesco and Min Zhang (ed), The 23rd International Conference on Formal Engineering Methods (ICFEM 2022).
Lecture Notes in Computer Science, volume 13478, pages 20-35.
© Springer-Verlag
Available: DOI

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn Talcott.
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2.
In proceedings of International Joint Conference on Automated Reasoning (IJCAR).
Lecture Notes in Computer Science, volume 13385, pages 529-540.
© Springer-Verlag
Available: DOI

Raúl López-Rueda, Santiago Escobar.
Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method.
In Kyungmin Bae (ed), 14th International Workshop on Rewriting Logic and Its Applications, WRLA 2022.
Lecture Notes in Computer Science, volume 13252, pages 45--64.
© Springer-Verlag
Available: DOI

Raúl López-Rueda, Santiago Escobar, Jose Meseguer.
An Efficient Canonical Narrowing Implementation for Protocol Analysis.
In Kyungmin Bae (ed), 14th International Workshop on Rewriting Logic and Its Applications, WRLA 2022.
Lecture Notes in Computer Science, volume 13252, pages 151--170.
© Springer-Verlag
Available: DOI

2020

Santiago Escobar and Narciso Martí-Oliet Rewriting Logic and Its Applications, 13th International Workshop, WRLA 2020, Virtual Event, October 20-22, 2020, Revised Selected Papers. Lecture Notes in Computer Science, volume 12328, 215 pages. © Springer-Verlag Available: DOI

Damián Aparicio-Sánchez, Santiago Escobar, Julia Sapiña.
Variant-based Equational Unification under Constructor Symbols.
In proceedings of the 36th International Conference on Logic Programming (ICLP 2020).
ICLP Technical Communications 2020. Electronic Proceedings in Theoretical Computer Science, volume 325, pages 38-51. 2020.
Available: DOI

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn Talcott
Programming and Symbolic Computation in Maude.
Journal of Logical and Algebraic Methods in Programming, volume 110, 2020.
© Elsevier Science
Available: DOI

2019

María Alpuente, Demis Ballis, Santiago Escobar, Julia Sapiña.
Symbolic Analysis of Maude Theories with Narval.
Theory and Practice of Logic Programming, 19(5-6): 874-890 (2019).
© Cambridge University Press
Available: DOI

Santiago Escobar, Julia Sapiña.
Most General Variant Unifiers.
In proceedings of the 35rd International Conference on Logic Programming (ICLP 2019).
ICLP Technical Communications 2019: 154-167, Electronic Proceedings in Theoretical Computer Science, 2019.
Available: DOI

Santiago Escobar, José Meseguer.
Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method.
In proceedings of Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows.
Lecture Notes in Computer Science, volume 11565, pages 15-38.
© Springer-Verlag
Available: DOI

2018

Santiago Escobar.
Multiparadigm programming in Maude.
In proceedings of 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018).
Lecture Notes in Computer Science, volume 11152, pages 26-44.
© Springer-Verlag
Available: DOI

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott.
Associative Unification and Symbolic Reasoning Modulo Associativity in Maude.
In proceedings of 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018).
Lecture Notes in Computer Science, volume 11152, pages 98-114.
© Springer-Verlag
Available: DOI

2017

María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, Julia Sapiña.
Inspecting Maude Variants with GLINTS.
Theory and Practice of Logic Programming, Volume 17, Issue 5-6, pages 689-707, September 2017.
© Cambridge University Press
Available: DOI

María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, Julia Sapiña.
Inspecting Maude Variants with GLINTS.
In proceedings of the 33rd International Conference on Logic Programming (ICLP 2017).
Available: CoRR

2016

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott.
Built-in Variant Generation and Unification, and their Applications in Maude 2.7.
In proceedings of International Joint Conference on Automated Reasoning (IJCAR).
Lecture Notes in Computer Science, volume 9706, pages 183-192. Springer 2016.
© Springer-Verlag
Available: DOI

2015

Andrew Cholewa, Santiago Escobar, José Meseguer
Constrained narrowing for conditional equational theories modulo axioms.
Science of Computer Programming, volume 112, part 1, pages 24-57, 2015,.
© Elsevier
Available: DOI

Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, Carolyn L. Talcott.
Two Decades of Maude.
In proceedings of Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday.
Lecture Notes in Computer Science, volume 9200, pages 232-254. Springer 2015.
© Springer-Verlag
Available: DOI

2014

Santiago Escobar.
Functional Logic Programming in Maude.
In proceedings of Specification, Algebra, and Software: A Festschrift Symposium in Honor of Kokichi Futatsugit (SAS 2014), Kanazawa, Japan, 2014.
Lecture Notes in Computer Science, volume 8373, pages 315-336, Springer 2014.
© Springer-Verlag
Available: Preliminary version DOI

2013

Santiago Escobar.
Unification and Anti-unification modulo Equational Theories.
The 27th International Workshop on Unification (UNIF 2013), EPiC - EasyChair Proceedings in Computing, volume 19, page 1, 2013.

Kyungmin Bae, Santiago Escobar, and José Meseguer.
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing.
In proceedings of 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
LIPIcs-Leibniz International Proceedings in Informatics, volume 21, pages 81-96, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Available: DOI

2012

Santiago Escobar, Ralf Sasse, José Meseguer.
Folding variant narrowing and optimal variant termination.
The Journal of Logic and Algebraic Programming, Volume 81, Issues 7-8, pages 898-928, 2012.
© Elsevier
Available: Preliminary version DOI link

2011

Francisco Durán, Steven Eker, Santiago Escobar, José Meseguer and Carolyn Talcott.
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (system description)
In proceedings of 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
LIPIcs-Leibniz International Proceedings in Informatics, volume 10, pages 31-40, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Available: DOI

2010

Santiago Escobar, José Meseguer, Ralf Sasse.
Folding Variant Narrowing and Optimal Variant Termination
In proceedings of 8th International Workshop on Rewriting Logic and its Applications (WRLA 2010),
LNCS 6381, pages 52-68. 2010.
© Springer-Verlag
Available: PDF DOI

2009

Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Pat Lincoln, Narciso Marti-Oliet, José Meseguer and Carolyn Talcott.
Unification and Narrowing in Maude 2.4 (system description)
In proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA'09), LNCS 5595, pages 380-390, 2009.
© Springer-Verlag
Available: DOI PDF

2008

Santiago Escobar, José Meseguer, Ralf Sasse.
Effectively Checking or Disproving the Finite Variant Property
In proceedings of 19th International Conference on Rewriting Techniques and Applications (RTA 2008),
LNCS 5117, pages 79-93. 2008.
© Springer-Verlag
Available: DOI PDF

Santiago Escobar, José Meseguer, Ralf Sasse.
Equational Unification by Variant Narrowing
In proceedings of 22nd International Workshop on Unification,
short paper, 2008

Santiago Escobar, José Meseguer, Ralf Sasse.
Variant Narrowing and Equational Unification
In proceedings of 7th International Workshop on Rewriting Logic and its Applications (WRLA08),
Electronic Notes in Theoretical Computer Science, volume 238, issue 3, pages 103-119, 2009
© Elsevier
Available: DOI PDF