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 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 programming languages such as Curry, Java, Erlang or Mozart/Oz. Research areas include operational semantics of concurrent programming languages, specification logics and proof systems, compositional verification techniques and lately the use of code rewriting techniques to enforce compliance with security properties instead of checking for compliance.

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 takes place within the ProTest (property based testing) European STREP project (FP7).