About me

I am a researcher at the Babel group at the Facultad de Informática, Universidad Politécnica de Madrid, working on formal techniques for constructing functionally correct software applications.

Academic History
MSc and PhLic from Uppsala University, Sweden. PhD from the Royal Institute of Technology, Stockholm, Sweden, 2001.
Researcher at the Swedish Institute of Computer Science (SICS), between 1990 and 2005.
Working on a Ramón and Cajal contract, now converted into a "profesor contratado" contract, at the Facultad de Informática, Universidad Politécnica de Madrid since 2005.

Research Interests
My current research focuses on reasoning formally about concurrent programs (on the level of real program code). That is, to support reasoning about programs in standard concurrent programming languages such as Java or Erlang. Research areas include operational semantics of concurrent programming languages, model checking, specification logics and proof systems, compositional verification techniques, and property-based testing.

In an earlier cooperation with Ericsson CSLAB the formal verification of Erlang code was explored using both theorem proving techniques and automated verification techniques.

Previous work includes the development of the McErlang software model checker for Erlang. The idea is to replace the part of the standard Erlang runtime system that concerns distribution, concurrency and communication with a new runtime system which simulates processes inside the model checker and which offers easy access to the program state. Our work on model checking took place within the ProTest (property based testing) European STREP project (FP7).

The recently concluded Prowess project European STREP project (FP7) was dedicated to developing and applying property-based testing techniques for web services and internet applications; including working extensively with, and extending the functionality of, Quviq QuickCheck.