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 and secure distributed 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 an "I3" 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.

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

I also took part in the Verificard project funded by the European Commission. The intent was to explore various state-of-the-art verification techniques to ensure various safety and security aspects of Smartcards programmed in the JavaCard subset of Java.

A current working theme focuses on 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).

We are now taking part in the Prowess project European STREP project (FP7) which is dedicated to developing and applying property-based testing techniques for web services and internet applications.