By Raúl López Rueda
On 29 October at 2:30 pm, in FC6 0.29, Raúl López Rueda will give a lecture entitled "From Term Rewriting to Folding Narrowing: Foundations and Applications".
Title:
From Term Rewriting to Folding Narrowing: Foundations and Applications
Abstract:
Term rewriting provides a general computational framework in which computations are described through the application of rewrite rules to terms. Narrowing can be viewed as a generalization of rewriting that combines rewriting with unification, thereby enabling symbolic reachability analysis over terms containing free variables.
This talk introduces the main ideas leading from term rewriting to narrowing, and ultimately to folding narrowing, a technique that can substantially improve narrowing in many cases by turning infinite or very large search trees into finite graphs. This makes it possible to reason about properties that would otherwise be beyond the reach of standard symbolic exploration.
The talk concludes with an overview of several extensions to narrowing developed in recent years, which make it possible to analyze broader classes of systems and verify more complex properties. It will also discuss the use of unification and narrowing mechanisms in tools for protocol analysis, such as Maude-NPA, and for invariant verification in concurrent systems, such as DM-Check.
Bio:
Raúl López Rueda is a researcher in formal methods at the VRAIN, Universitat Politècnica de València (UPV), Spain. He received his PhD in Computer Science from UPV in 2026.
His research focuses on symbolic verification techniques based on rewriting logic, with particular emphasis on narrowing, unification, and state-space reduction methods. He works on the development of advanced narrowing techniques aimed at making the symbolic analysis of concurrent and distributed systems more effective.
He has also contributed to the development of a verification tool based on Maude called DM-Check, a deductive model checker for the verification of invariants in concurrent systems. His broader research interests include automated reasoning, symbolic reachability analysis, inductive verification, and the practical application of formal methods to complex systems.