About
I am a researcher in computer science with a special interest in formal methods. Here is a recent picture of me:
Academic biography
As of February 2026, I am 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 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 verification of computer systems. In particular, I am interested in distributed database systems and consistency models. Feel free to get in touch if our interests align.Previously, I investigated decision procedures for logics of arrays. 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.
Publications
You can find my research works on dblp and/or orcid. Here are the main works:Formal Proofs
- Rodrigo Raya, Manuel Eberl: Gauss Sums and the Pólya-Vinogradov Inequality. Arch. Formal Proofs 2019 (2019)
- Thomas C. Hales, Rodrigo Raya: Formal Proof of the Group Law for Edwards Elliptic Curves. IJCAR (2) 2020: 254-269
- Rodrigo Raya: Group Law of Edwards Elliptic Curves. Arch. Formal Proofs 2023 (2023)
Decision Procedures
- Rodrigo Raya, Viktor Kunčak: On algebraic array theories. J. Log. Algebraic Methods Program. 136: 100906 (2024)
- Rodrigo Raya, Viktor Kunčak: Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. 140: 100978 (2024)
- Rodrigo Raya, Christophe Ringeissen: Modular derivation of decision procedures for extensions of the algebraic theory of arrays. J. Log. Algebraic Methods Program. 151: 101132 (2026)
- Rodrigo Raya, Jad Hamza, Viktor Kunčak: Convex and Reverse Convex Prequadratics Constraints for Decidable Logics of Relations with Cardinalities. ACM Transactions on Computational Logic. (2026)