Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Margus Veanes

Margus Veanes
SENIOR RESEARCHER
.

Short Bio

I am a researcher in the Research in Software Engineering area at Microsoft Research.

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; see project M3 . 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 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.

I live in Bellevue with my wife Katrine and our two sons Margus and Jaan. These pictures of Margus and Jaan were taken at the MSR picnic August 2008. Here is a picture of me with my wife at a Microsoft holiday party few years ago.

Selected Publications

    2015

    • Margus Veanes and Nikolaj Bjørner, Symbolic Tree Automata, in Information Processing Letters, vol. 115, no. 3, pp. 418-424, Elsevier, March 2015
    • Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits, Data-Parallel String-Manipulating Programs, in POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM – Association for Computing Machinery, January 2015
    • Robert A Cochran, Loris D’Antoni, Benjamin Livshits, David Molnar, and Margus Veanes, Program Boosting: Program Synthesis via Crowd-Sourcing, in POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM – Association for Computing Machinery, January 2015

    2014

    2013

    2012

    2011

    2010

    2009

    2008

    2007

    2006

    2005

    Older publications

      2005

      2004

      2003

      2002

      2001

      2000

      1999

      1998

      1997

      1996

      1995

      1993

      Links

      Projects

      • Automata: Microsoft Research Automata Toolkit
      • BEK: domain specific language for sanitizers
      • FAST: Functional Abstraction of Symbolic Transducers 
      • Bex: declarative language for string coders