| 2025 | CADE | Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems. | Salvador Lucas |
| 2024 | CSL | Confluence of Conditional Rewriting Modulo. | Salvador Lucas |
| 2024 | FSCD | Termination of Generalized Term Rewriting Systems. | Salvador Lucas |
| 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 | IJCAI | Proving Semantic Properties as First-Order Satisfiability (Extended Abstract). | Salvador Lucas |
| 2019 | CADE | Automatic Generation of Logical Models with AGES. | Ral Gutirrez, Salvador Lucas |
| 2018 | LOPSTR | Proving Program Properties as First-Order Satisfiability. | Salvador Lucas |
| 2017 | LOPSTR | Analysis of Rewriting-Based Systems as First-Order Theories. | Salvador Lucas |
| 2014 | AISC | Using Representation Theorems for Proving Polynomials Non-negative. | Salvador Lucas |
| 2014 | AISC | Models for Logics and Conditional Constraints in Automated Proofs of Termination. | Salvador Lucas, Jos Meseguer |
| 2014 | LOPSTR | Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems. | Salvador Lucas, Jos Meseguer, Ral Gutirrez |
| 2014 | PPDP | Proving Operational Termination of Declarative Programs in General Logics. | Salvador Lucas, Jos Meseguer |
| 2010 | AISC | From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals. | Salvador Lucas |
| 2009 | CADE | Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. | Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | AISC | Search Techniques for Rational Polynomial Orders. | Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jrgen Giesl, Salvador Lucas, Peter Schneider-Kamp |
| 2008 | CADE | MTT: The Maude Termination Tool (System Description). | Francisco Durn, Salvador Lucas, Jos Meseguer |
| 2008 | LPAR | Improving Context-Sensitive Dependency Pairs. | Beatriz Alarcn, Fabian Emmes, Carsten Fuhs, Jrgen Giesl, Ral Gutirrez, Salvador Lucas, Peter Schneider-Kamp, Ren Thiemann |
| 2008 | PPDP | Order-sorted dependency pairs. | Salvador Lucas, Jos Meseguer |
| 2007 | CALCO | The Maude Formal Tool Environment. | Manuel Clavel, Francisco Durn, Joe Hendrix, Salvador Lucas, Jos Meseguer, Peter Csaba lveczky |
| 2007 | PPDP | Practical use of polynomials over the reals in proofs of termination. | Salvador Lucas |
| 2005 | LPAR | Termination of Fair Computations in Term Rewriting. | Salvador Lucas, Jos Meseguer |
| 2004 | FOSSACS | Polynomials for Proving Termination of Context-Sensitive Rewriting. | Salvador Lucas |
| 2004 | PEPM | Proving termination of membership equational programs. | Francisco Durn, Salvador Lucas, Jos Meseguer, Claude March, Xavier Urbain |
| 2002 | CADE | Recursive Path Orderings Can Be Context-Sensitive. | Cristina Borralleras, Salvador Lucas, Albert Rubio |
| 2002 | LOPSTR | Abstract Diagnosis of Functional Programs. | Mara Alpuente, Marco Comini, Santiago Escobar, Moreno Falaschi, Salvador Lucas |
| 2002 | LPAR | Improving On-Demand Strategy Annotations. | Mara Alpuente, Santiago Escobar, Bernhard Gramlich, Salvador Lucas |
| 2002 | PPDP | Modular termination of context-sensitive rewriting. | Bernhard Gramlich, Salvador Lucas |
| 2001 | LPAR | Termination of Rewriting With Strategy Annotations. | Salvador Lucas |
| 2001 | PPDP | Termination of On-Demand Rewriting and Termination of OBJ Programs. | Salvador Lucas |
| 1999 | FLOPS | A Semantics for Program Analysis in Narrowing-Based Functional Logic Languages. | Michael Hanus, Salvador Lucas |
| 1999 | ICFP | Specialization of Inductively Sequential Functional Logic Programs. | Mara Alpuente, Michael Hanus, Salvador Lucas, Germn Vidal |
| 1999 | SOFSEM | UPV-CURRY: An Incremental CURRY Interpreter. | Mara Alpuente, Santiago Escobar, Salvador Lucas |
| 1997 | SOFSEM | Efficient Strong Sequentiality Using Replacement Restrictions. | Salvador Lucas |
| 1996 | ICALP | Termination of Context-Sensitive Rewriting by Rewriting. | Salvador Lucas |
| 1996 | SOFSEM | A New Proposal of Concurrent Process Calculus. | Salvador Lucas, Javier Oliver |
| 1995 | SOFSEM | Fundamentals of Context=Sensitive Rewriting. | Salvador Lucas |