Publications - Logical Model Checking

2026

Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, Jose Meseguer, Julia Sapiña
DM-Check: Verifying invariants of concurrent systems by deductive model checking.
Journal of Logical and Algebraic Methods in Programming, Volume 149, March 2026, 101107.
© Elsevier Science
Available: DOI

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), 10-11 September 2025, Rende, Italy.
Article number 4, 14 pages, 2025.
© ACM Press
Available: DOI

2024

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

2023

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, Volume 135, July 2023. 2023
© Elsevier Science
Available: DOI

2019

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

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

2007

Santiago Escobar, José Meseguer
Symbolic Model Checking of Infinite-State Systems Using Narrowing
In proceedings of 18th International Conference on Rewriting Techniques and Applications (RTA 2007).
To appear, 2007.
© Springer-Verlag
Available: PDF