| 2022 | LOPSTR | Confluence Framework: Proving Confluence with CONFident. | Ral Gutirrez, Miguel Vtores, Salvador Lucas |
| 2020 | CADE | Automatically Proving and Disproving Feasibility Conditions. | Ral Gutirrez, Salvador Lucas |
| 2020 | CADE | mu-term: Verify Termination Properties Automatically (System Description). | Ral Gutirrez, Salvador Lucas |
| 2020 | ESORICS | An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA. | Damin Aparicio-Snchez, Santiago Escobar, Ral Gutirrez, Julia Sapia |
| 2019 | CADE | Automatic Generation of Logical Models with AGES. | Ral Gutirrez, Salvador Lucas |
| 2017 | LOPSTR | Variant-Based Decidable Satisfiability in Initial Algebras with Predicates. | Ral Gutirrez, Jos Meseguer |
| 2014 | LOPSTR | Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems. | Salvador Lucas, Jos Meseguer, Ral Gutirrez |
| 2013 | LOPSTR | A Transformational Approach to Resource Analysis with Typed-Norms. | Elvira Albert, Samir Genaim, Ral Gutirrez |
| 2008 | LPAR | Improving Context-Sensitive Dependency Pairs. | Beatriz Alarcn, Fabian Emmes, Carsten Fuhs, Jrgen Giesl, Ral Gutirrez, Salvador Lucas, Peter Schneider-Kamp, Ren Thiemann |