My current research agenda is to develop scalable analysis techniques and corresponding logical foundations for analysis of programs manipulating strings (see projects BEK and REX that build upon the Automata toolkit). I am also investigating foundations for behavioral model analysis in the context of model validation and model-based testing. The main focus is on the use of symbolic automata theory in combination with state-of-the-art satisfiability modulo theories techniques.
My prior research was focused on model-based testing; I was a co-designer and co-developer of Spec Explorer 2004, and I am a co-author of the book Model-Based Software Testing and Analysis with C#, Cambridge University Press, 2008.
I defended my PhD thesis at Uppsala University in June 1997 in the area of theorem proving and decision problems in first-order logic with equality, with Andrei Voronkov as my supervisor. From August 1997 to June 1999, I worked as a postdoc in the Programming Logic group headed by Harald Ganzinger, at Max Planck Institute for Computer Science in Saarbruecken. I joined MSR in July 1999.