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# (opens in new tab), Cambridge University Press, 2008.

I defended my PhD thesis (opens in new tab) at Uppsala University (opens in new tab) in June 1997 in the area of theorem proving and decision problems in first-order logic with equality, with Andrei Voronkov (opens in new tab) as my supervisor. From August 1997 to June 1999, I worked as a postdoc in the Programming Logic group headed by Harald Ganzinger (opens in new tab), at Max Planck Institute for Computer Science (opens in new tab) in Saarbruecken. I joined MSR in July 1999.