Short Bio
I am a researcher in the Foundations of Software Engineering or FSE group since 1999. FSE is part of the Research in Softare 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 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.
2012
- Margus Veanes and Nikolaj Bjorner, Symbolic Automata: The Toolkit, in TACAS'12, Springer Verlag, March 2012
- Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjorner, Symbolic Finite State Transducers: Algorithms and Applications, in POPL’12, ACM SIGPLAN, January 2012
2011
- Margus Veanes, David Molnar, Benjamin Livshits, and Lubomir Litchev, Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration, no. MSR-TR-2011-124, November 2011
- Margus Veanes and Nikolaj Bjorner, Alternating simulation and IOCO, in International Journal on Software Tools for Technology Transfer (STTT) , Springer, November 2011
- Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes, Fast and Precise Sanitizer Analysis with BEK, in USENIX Security'11, August 2011
- nikolaj bjorner, pieter hooimeijer, benjamin livshits, david molnar, and margus veanes, Symbolic Finite State Transducers: Algorithms and Applications, no. MSR-TR-2011-85, 14 July 2011
- Margus Veanes, David Molnar, and Benjamin Livshits, Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers, no. MSR-TR-2011-32, 14 March 2011
- Nikolaj Bjorner and Margus Veanes, Symbolic Transducers, no. MSR-TR-2011-3, 21 January 2011
- Pieter Hooimeijer and Margus Veanes, An Evaluation of Automata Algorithms for String Analysis, in VMCAI 2011, Springer Verlag, January 2011
- Margus Veanes and Nikolaj Bjorner, Symbolic Tree Transducers, in Ershov Informatics Conference (PSI'11), Springer, 2011
2010
- Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes, BEK: Modeling Imperative String Operations with Symbolic Transducers, no. MSR-TR-2010-154, 26 November 2010
- Margus Veanes and Nikolaj Bjorner, Alternating Simulation and IOCO, in ICTSS'10, Springer Verlag, November 2010
- Margus Veanes and Jonathan Jacky, Composing Model Programs for Analysis, in The Journal of Logic and Algebraic Programming, vol. 79, no. 7, pp. 467-482, Elsevier , October 2010
- Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura, Symbolic Automata Constraint Solving, in LPAR-17, Springer Verlag, October 2010
- Pieter Hooimeijer, Margus Veanes, Prateek Saxena, and David Molnar, Modeling Imperative String Operations with Transducers, no. MSR-TR-2010-96, July 2010
- Pieter Hooimeijer and Margus Veanes, An Evaluation of Automata Algorithms for String Analysis, no. MSR-TR-2010-90, July 2010
- Margus Veanes and Nikolaj Bjorner, Alternating Simulation and IOCO, no. MSR-TR-2010-38, April 2010
- Margus Veanes, Nikolai Tillmann, and Peli de Halleux, Qex: Symbolic SQL Query Explorer, in LPAR-16, Springer Verlag, April 2010
- Margus Veanes, Peli de Halleux, and Nikolai Tillmann, Rex: Symbolic Regular Expression Explorer, in Third International Conference on Software Testing, Verification and Validation (ICST) , IEEE, April 2010
2009
- Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura, Solving Extended Regular Constraints Symbolically, no. MSR-TR-2009-177, December 2009
- Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann, Symbolic Query Exploration, in ICFEM'09, Springer Verlag, December 2009
- Juhan Ernits, Rivo Roo, Jonathan Jacky, and Margus Veanes, Model-Based Testing of Web Applications using NModel, in TESTCOM/FATES 2009, Springer Verlag, 2 November 2009
- Margus Veanes, Peli de Halleux, and Nikolai Tillmann, Rex: Symbolic Regular Expression Explorer, no. MSR-TR-2009-137, October 2009
- Margus Veanes, Nikolai Tillmann, and Jonathan de Halleux, Qex: Symbolic SQL Query Explorer, no. MSR-TR-2009-2015, October 2009
- Margus Veanes, Nikolaj Bjorner, Yuri Gurevich, and Wolfram Schulte, Symbolic Bounded Model Checking of Abstract State Machines, in Int J Software Informatics, vol. 3, no. (2-3), pp. 149-170, June 2009
- Margus Veanes and Nikolaj Bjorner, Symbolic Bounded Conformance Checking of Model Programs, in Perspectives of System Informatics (PSI'09), Springer Verlag, June 2009
- Margus Veanes and Nikolaj Bjorner, Input-Output Model Programs, no. MSR-TR-2009-56, May 2009
- Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann, Symbolic Query Exploration, no. MSR-TR-2009-65, May 2009
- Margus Veanes and Nikolaj Bjorner, Symbolic Bounded Conformance Checking of Model Programs, no. MSR-TR-2009-28, 14 March 2009
- Johannes Helander and Margus Veanes, Arranging Partitures for Models and Theorems, no. MSR-TR-2009-24, March 2009
2008
- Margus Veanes and Ando Saabas, On Bounded Reachability of Programs with Set Comprehensions, in LPAR'08, Springer Verlag, November 2008
- Margus Veanes and Ando Saabas, Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract), in ABZ'08, Springer Verlag, September 2008
- Juhan Ernits, Margus Veanes, and Johannes Helander, Model-Based Testing of Robots with NModel, in TestCom/FATES 2008 Short Papers, June 2008
- Margus Veanes, Nikolaj Bjørner, and Alexander Raschke, An SMT Approach to Bounded Reachability Analysis of Model Programs, in FORTE'08, Springer Verlag, June 2008
- Margus Veanes and Wolfram Schulte, Protocol Modeling with Model Program Composition, in FORTE'08, Springer Verlag, June 2008
- Margus Veanes, Ando Saabas, and Nikolaj Bjorner, Bounded reachability of model programs, no. MSR-TR-2008-81, May 2008
- Johannes Helander and Margus Veanes, Enabling the Future Auto with Model-Driven Services, in National Workshop on High-Confidence Automotive Cyber-Physical Systems., April 2008
- Jonathan Jacky, Margus Veanes, Colin Campbell, and Wolfram Schulte, Model-Based Software Testing and Analysis with C#, Cambridge University Press, January 2008
- Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson, Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, in Formal Methods and Testing, vol. 4949, pp. 39-76, Springer Verlag, 2008
2007
- Johannes Helander, Risto Serg, Margus Veanes, and Pritam Roy, Adapting Futures: Scalability for Real-World Computing, in RTSS'07, IEEE Computer Society, December 2007
- Oscar Almeida, Alessandro Forin, Philip Garcia, Johannes Helander, Nishith Khantal, Hong Lu, Karl Meier, Sibin Mohan, Henrik Nielsen, Richard Neil Pittman, Risto Serg, Bharat Sukhwani, Margus Veanes, Benjamin G. Zorn, Sarah Berry, Chris Boyce, David Chaszar, Brandon Culrich, Mikhail Kisin, Gabe Knezek, Warren Linam-Church, Steve Liu, Michael Stewart, and Doug Toney, Embedded Systems Research at DemoFest’07, no. MSR-TR-2007-94, July 2007
- Margus Veanes, Juhan Ernits, and Colin Campbell, State Isomorphism in Model Programs with Abstract Data Structures, in FORTE'07, Springer Verlag, June 2007
- Margus Veanes, Colin Campbell, and Wolfram Schulte, Composition of Model Programs, in FORTE, Springer Verlag, June 2007
- Yuri Gurevich, Margus Veanes, and Charles Wallace, Can Abstract State Machines Be Useful in Language Theory?, in Theoretical Computer Science, vol. 376, no. 1, pp. 17-29, Elsevier , 2007
- Margus Veanes, Colin Campbell, and Wolfram Schulte, Parallel and Serial Composition of Model Programs, no. MSR-TR-2007-22, 2007
2006
- Yuri Gurevich, Margus Veanes, and Charles Wallace, Can Abstract State Machines Be Useful in Language Theory?, no. MSR-TR-2006-159, November 2006
- Margus Veanes, Pritam Roy, and Colin Campbell, Online Testing with Reinforcement Learning, in Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006, Springer Verlag, 2006
2005
- Wolfgang Grieskamp, Nikolai Tillmann, Colin Campbell, Wolfram Schulte, and Margus Veanes, Action Machines - Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation, in Quality Software, 2005. (QSIC 2005). Fifth International Conference on , IEEE Computer Society, September 2005
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to Test, in FATES 2005, Springer Verlag, July 2005
- Colin Campbell, Margus Veanes, Jiale Huo, and Alexandre Petrenko, Multiplexing of Partially Ordered Events, in TestCom 2005, Springer Verlag, June 2005
- Colin Campbell and Margus Veanes, Exploration with Multiple State Groupings, in Abstract State Machines 2005, 2005
- Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Testing Concurrent Object-Oriented Systems with Spec Explorer, in FM, Springer, 2005
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to test, no. MSR-TR-2005-04, January 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Pushmeet Kohli, On-The-Fly Testing of Reactive Systems, no. MSR-TR-2005-05, January 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann, Online testing with model programs, in ESEC/SIGSOFT FSE, ACM, 2005
2004
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, Abstract Communication Model for Distributed Systems, in IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol. 30, no. 7, pp. 1-15, IEEE Computer Society, July 2004
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Towards a Tool Environment for Model-Based Testing with AsmL, in FATES 2003, Springer Verlag, 2004
- Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, and Wolfgang Grieskamp, Optimal strategies for testing nondeterministic systems, in ISSTA 2004, ACM, 2004
- Wolfgang Grieskamp, Nikolai Tillmann, and Margus Veanes, Instrumenting Scenarios in a Model-Driven Development Environment, in Journal of Information and Software Technology, vol. 46, no. 15, pp. 1027-1036, Elsevier , 2004
2003
- Wolfgang Grieskamp, Lev Nachmanson, Nikolai Tillmann, and Margus Veanes, Test Case Generation from AsmL Specifications, in ASM 2003, Springer Verlag, March 2003
- Michael Barnett, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Validating Use-Cases with the AsmL Test Tool, in QSIC, IEEE Computer Society, 2003
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Model-Based Testing with AsmL .NET, in 1st European Conference on Model-Driven Software Engineering, 2003
- Margus Veanes and Rostislav Yavorsky, Combined Algorithm for Approximating a Finite State Abstraction of a Large System, in ICSE 2003/Scenarios Workshop, 2003
2002
- Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Generating finite state machines from abstract state machines, in ISSTA 2002, July 2002
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, An Abstract Communication Model, no. MSR-TR-2002-55, May 2002
- Uwe Glässer and Margus Veanes, Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines, in Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002), Kluwer Academic , 2002
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, High-level Executable Specification of the Universal Plug and Play Architecture, in HICSS 2002, IEEE Computer Society, 2002
- Margus Veanes, Modeling Software: From Theory to Practice, in FSTTCS 2002, Springer Verlag, 2002
2001
- Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Toward Industrial Strength Abstract State Machines, no. MSR-TR-2001-98, October 2001
- U. Glässer, Y. Gurevich, and M. Veanes, Universal Plug and Play Machine Models, no. MSR-TR-2001-59, June 2001
- Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Conformance Testing with Abstract State Machines, in EUROCAST 2001, February 2001
2000
- Margus Veanes, Farmer's Theorem revisited, in Information Processing Letters, vol. 74, no. 1-2, pp. 47-53, Elsevier , April 2000
- Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov, Decidability and complexity of simultaneous rigid E-unification with one variable and related results, in Theoretical Computer Science, vol. 243, no. 1-2, pp. 167-184, Elsevier , 2000
- Jordi Levy and Margus Veanes, On the Undecidability of Second-Order Unification, in Information and Computation, vol. 159, no. 1-2, pp. 125-150, 2000
- Harald Ganzinger, Florent Jacquemard, and Margus Veanes, Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification, in International Journal of Foundations of Computer Science , vol. 11, no. 1, pp. 3-27, World Scientific Publishing, 2000
1999
- Margus Veanes and Yuri Gurevich, Logic with Equality: Partisan Corroboration and Shifted Pairing, in Information and Computation, vol. 152, no. 2, pp. 205-235, August 1999
- Harald Ganzinger, Christoph Meyer, and Margus Veanes, The Two-Variable Guarded Fragment with Transitive Relations, in LICS 1999, IEEE Computer Society, 1999
- Véronique Cortier, Harald Ganzinger, Florent Jacquemard, and Margus Veanes, Decidable Fragments of Simultaneous Rigid Reachability, in ICALP 1999, Springer Verlag, 1999
1998
- Margus Veanes, The relation between second-order unification and simultaneous rigid E-unification, in Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98), IEEE Computer Society, June 1998
- Margus Veanes, The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification, no. MPI-I-98-2-005, February 1998
- Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov, The decidability of simultaneous rigid E-unification with one variable, in RTA'98, Springer Verlag, 1998
- Harald Ganzinger, Florent Jacquemard, and Margus Veanes, Rigid reachability, in Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98), Springer Verlag, 1998
- Jordi Jevy and Margus Veanes, On Unification Problems in Restricted Second-Order Languages, in Annual Conference of the European Association for Computer Science Logic, CSL'98, 1998
1997
- Margus Veanes, On Simultaneous Rigid E-Unification, pp. 120, Uppsala University, June 1997
- Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov, The decidability of simultaneous rigid E-unification with one variable, no. 139, April 1997
- Yuri Gurevich and Margus Veanes, Some undecidable problems related to the Herbrand theorem, no. 138, March 1997
- Margus Veanes, The undecidability of simultaneous rigid E-unification with two variables, in 5th Kurt Gödel Colloquium (KGC'97), Springer Verlag, 1997
- Margus Veanes, On Computational Complexity of Basic Decision Problems of Finite Tree Automata, no. 133, January 1997
1996
- Margus Veanes, Uniform representation of recursively enumerable sets with simultaneous rigid E-unification, no. 126, June 1996
- Margus Veanes, Uniform representation of recursively enumerable sets with simultaneous rigid E-unification (extended abstract), in Proc. 10th International Workshop on Unification (UNIF'96), 1996
- Margus Veanes and Jonas Barklund, Construction of natural cycletrees, in Information Processing Letters, vol. 60, pp. 313-318, Elsevier , 1996
- Margus Veanes and Jonas Barklund, Natural cycletrees: Flexible interconnection graphs, in Journal of Parallel and Distributed Computing, vol. 33, no. 1, pp. 44-54, 1996
- Margus Veanes and Jonas Barklund, On the number of edges in cycletrees, in Information Processing Letters, vol. 57, pp. 225-229, Elsevier , 1996
1995
- Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, and Margus Veanes, Meta-programming with Theory Systems, no. 106, May 1995
- Margus Veanes and Jonas Barklund, Cycletrees: Flexible Interconnection Graphs for Parallel Computing , no. 97, February 1995
- Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, and Margus Veanes, Meta-Programming with Theory Systems, in Meta-Logics and Logic Programming, pp. 195-224, MIT Press, 1995
1993
- Margus Veanes, Cycletrees: a Novel Class of Interconnection Graphs, Computing Science Department, Uppsala University, 1993



