Lazaro Alberto Larrauri Borroto

Formal Methods, PhD Student

Lazaro Alberto Larrauri Borroto joined IAIK in 2020 and is a member of the Systematic Construction of Correct Systems group. He holds a MSc degree in Mathematics and Mathematical Engineering from the Technical University of Barcelona. Alberto's research interests lie primarily in the area of automata learning, formal testing and verification, and model checking.

Office room: IF02060

Lazaro Alberto Larrauri Borroto


I recently started my PhD and I’m deeply diving into the topic of automata learning.

The research in the direction of automata learning includes basic research as well as applied research. There are still many open fundamental research questions left that I’m excited to explore and to develop new theory. The recent great success of applying automata learning in new application areas such as machine learning raises new problems and questions that are not visible when considering theory only. This results in an immense benefit from the connection between theory, implementation and application in the field of automata learning and in my PhD.



I assisted in the course Model Checking (practicals) where we teach among others:

  •  modeling reactive systems
  • temporal logics: CTL, LTL, CTL*
  • model checking algorithms for CTL and LTL

Looking for a bachelor’s thesis, or master’s thesis in automata learning?

Let me know and sent me an email. I have always open topics, both theoretical and practical ones,
and I’m looking forward to working with you!