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 main research interests are in model-based software development, testing and verification. I am a co-designer and co-developer of Spec Explorer 2004. The next generation Spec Explorer tool is being developed in the Windows organization. I am also a coordinator and developer of the open source NModel project and and a co-author of the book "Model-Based Software Testing and Analysis with C#", Cambridge University Press, 2008.
My current research agenda is to develop analysis techniques and corresponding logical foundations in order to analyze high-level models; see project M3. The main focus is on the use of theorem proving techniques to enable light-weight formal method support.
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.
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 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
- Nikolaj Bjorner, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Symbolic Bounded Model Checking of Abstract State Machines, no. MSR-TR-2009-14, February 2009
- Margus Veanes and Jonathan Jacky, Composing Model Programs for Analysis, in JLAP, Elsevier , 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
- Margus Veanes and Wolfram Schulte, Protocol Modeling with Model Program Composition, in FORTE'08, Springer Verlag, 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
- Juhan Ernits, Margus Veanes, and Johannes Helander, Model-Based Testing of Robots with NModel, in TestCom/FATES 2008 Short Papers, June 2008
- Margus Veanes, Ando Saabas, and Nikolaj Bjorner, Bounded reachability of model programs, no. MSR-TR-2008-81, May 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, 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
- Margus Veanes, Colin Campbell, and Wolfram Schulte, Parallel and Serial Composition of Model Programs, no. MSR-TR-2007-22, 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
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
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to test, no. MSR-TR-2005-04, January 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
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann, Online testing with model programs, in ESEC/SIGSOFT FSE, ACM, 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Pushmeet Kohli, On-The-Fly Testing of Reactive Systems, no. MSR-TR-2005-05, January 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
- Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, and Wolfgang Grieskamp, Optimal strategies for testing nondeterministic systems, in ISSTA 2004, ACM, 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
- 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, Yuri Gurevich, and Margus Veanes, High-level Executable Specification of the Universal Plug and Play Architecture, in HICSS 2002, IEEE Computer Society, 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
- 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, no. 17/93, Computing Science Department, Uppsala University, 1993
Links
Projects
- M3: Model theory, Model generation & Model analysis.
- AsmL: Abstract State Machine Language
- AsmL on codeplex
- NModel on codeplex.
- SpecExplorer 2004
- Qex: symbolic Query EXploration
Book
Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte: Model-Based Software Testing and Analysis with C#,
Cambridge University Press, 2008.




