I am a researcher in the Foundations of Software Engineering group at Microsoft Research since summer 1999. My main research interests are in model-based software development and testing. My main research goal is to help making the use of formal specifications and model-based testing a reality in the real life software development process. In this context I've been working on developing model-based testing technology, including efficient search and pruning techniques for exploring infinite state systems, testing of non-deterministic and distributed systems, using game theory and the theory of abstract state machines by Yuri Gurevich.

I am a co-designer and co-developer of the Spec Explorer tool that is part of the SpecExplorer distribution and have been working closely with Microsoft product groups in bringing this technology into their practice.

I got my Masters degree from Uppsala University in 1990, where I also defended my PhD in 1997 in the area of theorem proving, finite tree automata, and decision problems in first-order logic, under the supervision of Andrei Voronkov. From 1997 to mid 1999 I did my post graduate studies in the Programming Logic group headed by Harald Ganzinger, at the Max Planck Institute for Computer Science in Saarbruecken. There I studied second-order unification problems, their relations to fundamental decision problems in automated theorem proving with equality, and decision problems for the guarded fragment of first-order logic that arises by translation from modal-logics.