About
I am a researcher in computer science with a special interest in formal methods. Here is a picture that should help you recognise me in real life:
Academic biography
As of February 2026, I will be a lecturer in computer systems at the Polytechnic University of Madrid (Spain). Previously I was a visiting researcher at the INRIA Research Center in Nancy (France). Before that I was a postdoctoral researcher at the Max-Planck Institute for Software Systems in Kaiserslautern (Germany). I obtained my PhD in Computer Science at the Federal Polytechnic School of Lausanne (Switzerland). I hold two Bachelor Degrees, in Mathematics and Computer Engineering, from the University of Granada (Spain) for which I was awarded the Extraordinary Prize of Degree.Research
My current research interests lie in the interaction between decision procedures and learning algorithms in the context of logics of sequences.Previously, I investigated decision procedures for logics of sequences. In particular, my main research goal was to perform an in-depth analysis of specifications languages for programs manipulating unbounded data structures. Using results from classical model theory I described logical fragments with reasonable decision complexity and I investigated automated reasoning techniques such as combination of theories or interpolation which makes these fragments applicable in various software verification scenarios. In my work, I repeatedly found that supporting componentwise specifications is both a useful and relatively unexplored area of research.
I also have experience with the design of software verifiers and the use of proof assistants. Some of the proofs I wrote in Isabelle are available in the Archive or Formal Proofs and I even wrote a paper about one of them together with Thomas Hales. In particular, the Isabelle proof of the group law of Edwards curves is an example of the power of modern formal methods tools.