Portrait of Margus Veanes

Margus Veanes

Principal Researcher


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.