Raúl López Rueda

About Me

I am Raúl López-Rueda, a PhD researcher at the Universitat Politècnica de València (Valencia, Spain). My research focuses on formal methods, in particular on optimizing rewriting theories through narrowing-based techniques in Maude. I work on advancing symbolic analysis techniques for rewriting logic, with applications in areas such as concurrent systems and security protocols.

My contributions include the development of a canonical narrowing approach that incorporates irreducibility constraints, which significantly improves performance and reduces the search space in rewriting systems with variant equations. I also work on an extension that integrates conditional rewriting systems with SMT constraints, enabling more expressive and precise system specifications.

In addition, I contribute to the development of DM-Check, a deductive model checker that uses narrowing as the underlying exploration mechanism and relies on NuITP for invariant proving. This tool is designed to enhance deductive verification by combining symbolic exploration with powerful invariant checking techniques.

I am currently pursuing my PhD under the supervision of two experts in the Maude framework. Santiago Escobar, one of my advisors, is part of the Maude development team, which gives our work direct impact on the evolution of the system. My other advisor, Julia Sapiña, has extensive expertise in Maude, particularly in the design and implementation of systems and techniques in this language.