Margus Veanes Microsoft Research One Microsoft Way Building: B99, Room 2228 Redmond, WA 98052, USA Email : margus at microsoft dot com Phone : +1(425)705-2609 Fax : +1(425)936-7329 http://research.microsoft.com/~margus/ How to get to MSR, Redmond Links Short Bio Publications Book Projects

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.

Check also in digital libraries such as DBPL and CiteSeer.

2008

• Margus Veanes, Ando Saabas: On Bounded Reachability of Programs with Set Comprehensions. LPAR 2008.
• Margus Veanes, Nikolaj Bjørner, Alexander Raschke: An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE 2008: 53-68
• Margus Veanes, Ando Saabas: Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract). ABZ 2008: 355
• Margus Veanes, Ando Saabas, Nikolaj Bjørner, Bounded reachability of model programs, MSR Technical Report, MSR-TR-2008-81.
• Juhan Ernits, Margus Veanes, Johannes Helander: Model-Based Testing of Robots with NModel, TestCom/FATES 2008 Short Papers, Pages: 40-49
• Margus Veanes, Wolfram Schulte: Protocol Modeling with Model Program Composition. FORTE 2008: 324-339
• Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson: Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Formal Methods and Testing 2008: 39-76
• Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte, "Model-Based Software Testing and Analysis with C#", Cambridge University Press

2007

• Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy. Adapting Futures: Scalability for Real-World Computing. RTSS 2007.
• Margus Veanes, Juhan P. Ernits, Colin Campbell: State Isomorphism in Model Programs with Abstract Data Structures. FORTE 2007: 112-127
• M. Veanes, C. Campbell, and W. Schulte. Composition of Model Programs. FORTE 2007, LNCS vol. 4574, pages 128-142.
• Y. Gurevich, M. Veanes, and Charles Wallace, Can Abstract State Machines Be Useful in Language Theory?, Theoretical Computer Science.
• M. Veanes, C. Campbell, and W. Schulte, Parallel and Serial Composition of Model Programs, Microsoft Research Technical Report MSR-TR-2007-22.

2006

• M. Veanes and P. Roy and C. Campbell, Online Testing with Reinforcement Learning, Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006, volume 4262 of LNCS, pages 240-253, 2006.

2005

• Colin Campbell, Margus Veanes: State Exploration with Multiple State Groupings. Abstract State Machines 2005: 119-130
• Margus Veanes, Colin Campbell, Wolfram Schulte, Nikolai Tillmann: Online testing with model programs. ESEC/SIGSOFT FSE 2005: 273-282
• Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes: Play to Test. FATES 2005: 32-46
• Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes: Play to Test, Microsoft Research Technical Report MSR-TR-2005-04 (extended version of FATES 2005 paper)
• Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes: Testing Concurrent Object-Oriented Systems with Spec Explorer. FM 2005: 542-547
• Wolfgang Grieskamp, Nikolai Tillmann, Colin Campbell, Wolfram Schulte, Margus Veanes: Action Machines - Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation. QSIC 2005: 72-82
• Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko: Multiplexing of Partially Ordered Events. TestCom 2005: 97-110 (BEST PAPER award)
• M. Veanes, C. Campbell, W. Schulte, N. Tillmann, Online testing with model programs, ESEC/FSE-13; pages 273-282, ACM press.
• M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, L. Nachmanson, Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, Microsoft Research Technical Report MSR-TR-2005-59, 2005. (preliminary version of a chapter in the book Formal Methods and Testing)

2004

• L. Nachmanson, M. Veanes, W. Schulte, N. Tillmann and W. Grieskamp. Optimal Strategies for Testing Nondeterministic Systems. ISSTA'04, Software Engineering Notes, vol. 29, no. 4, 2004.
• U. Glässer, Y. Gurevich and M. Veanes. Abstract Communication Model for Distributed Systems. IEEE Transactions on Software Engineering, vol. 30, no. 7, pages 458 - 472, 2004.
• W. Grieskamp, N. Tillmann and M. Veanes. Instrumenting Scenarios in a Model-Driven Development Environment, Journal of Information and Software Technology, vol. 46, no. 15, pages 1027 - 1036, 2004
• M. Barnett, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann and M. Veanes. Towards a tool environment for model-based testing with AsmL. In Petrenko and Ulrich, editors, Formal Approaches to Software Testing, FATES 2003, volume 2931 of LNCS, pages 264--280. Springer, 2004.

2003

• M. Barnett, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann, and M. Veanes. Model-Based Testing with AsmL .NET. In proc 1st European Conference on Model-Driven Software Engineering, pp 12-19, 2003.
• M. Barnett, W. Grieskamp, W. Schulte, N. Tillmann, and M. Veanes. Validating Use-Cases with the AsmL Test Tool. Third International Conference on Quality Software. QSIC'2003, 2003.
• Wolfgang Grieskamp, Lev Nachmanson, Nikolai Tillmann, Margus Veanes: Test Case Generation from AsmL Specifications. Abstract State Machines 2003: 413
• M. Veanes and R. Yavorsky. Combined Algorithm for Approximating a Finite State Abstraction of a Large System. ICSE 2003/Scenarios Workshop. 2003.

2002

• W. Grieskamp, Y. Gurevich, W. Schulte and M. Veanes. Generating Finite State Machines from Abstract State Machines in ISSTA 2002, International Symposium on Software Testing and Analysis , July 2002.
• U. Glässer and M. Veanes, Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines. In proc Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress - TC10 Stream on Distributed and Parallel Embedded Systems (DIPES 2002), Kluwer Academic Publishers, 2002
• U. Glässer, Y.Gurevich and M. Veanes, An Abstract Communication Model. Foundations of Software Engineering, Microsoft Research, Microsoft Corporation, Technical Report, MSR-TR-2002-55, May 2002.
• U. Glässer, Y.Gurevich and M. Veanes, High-level Executable Specification of the Universal Plug and Play Architecture. In Proc. of 35th Hawaii International Conference on System Sciences, Software Technology Track, Domain-Specific Languages for Software Engineering, IEEE 2002.
• M. Veanes. Modeling Software: From Theory to Practice, FSTTCS 2002, Kanpur, India. LNCS, 2002. (invited talk).

2001

• W.Grieskamp, Y.Gurevich, W. Schulte and M. Veanes. Testing with Abstract State Machines. Formal Methods and Tools for Computer Science - EUROCAST'01 - Extended Abstracts , February 2001.
• Y. Gurevich, W. Schulte and M. Veanes, Toward Industrial Strength Abstract State Machines, in Proc ASM 2001, 2001.

2000

• Michael Barnett, Egon Börger, Yuri Gurevich, Wolfram Schulte, Margus Veanes: Using Abstract State Machines at Microsoft: A Case Study. Abstract State Machines 2000: 367-379
• Jordi Levy, Margus Veanes: On the Undecidability of Second-Order Unification. Inf. Comput. 159(1-2): 125-150 (2000)
• Margus Veanes: Farmer's Theorem revisited. Inf. Process. Lett. 74(1-2): 47-53 (2000)
• Harald Ganzinger, Florent Jacquemard, Margus Veanes: Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification. Int. J. Found. Comput. Sci. 11(1): 3-27 (2000)
• Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov: Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theor. Comput. Sci. 243(1-2): 167-184 (2000)

1999

• Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes: Decidable Fragments of Simultaneous Rigid Reachability. ICALP 1999: 250-260
• Harald Ganzinger, Christoph Meyer, Margus Veanes: The Two-Variable Guarded Fragment with Transitive Relations. LICS 1999: 24-34
• Yuri Gurevich, Margus Veanes: Logic with Equality: Partisan Corroboration and Shifted Pairing. Inf. Comput. 152(2): 205-235 (1999)

1998

• H. Ganzinger, F. Jacquemard and M. Veanes. Rigid reachability. Asian Computing Science Conference (ASIAN 98), Manila, The Philippines, December 8--10, 1998.
• J. Levy and M. Veanes. On unification problems in restricted second-order languages, CSL'98.
• M. Veanes. The relation between second-order unification and simultaneous rigid E-unification. In Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science, June 21-24, 1998, Indianapolis, Indiana (LICS'98), pages 264-275, IEEE Computer Society, 1998.
• A. Degtyarev, Yu. Gurevich, P. Narendran, M. Veanes, and A. Voronkov. The decidability of simultaneous rigid E-unification with one variable. In T. Nipkow, editor, Proc. RTA'98, volume 1379 of Lecture Notes in Computer Science, pages 181-195, Springer, 1998.
• J. Levy and M. Veanes. On unification problems in restricted second-order languages (abstract). In Proc. UNIF 98, 12th International Workshop on Unification, Rome, 29/06-01/07 1998, page 49, Research Report SI-98/8, Univ. of Rome, June 1998.
• M. Veanes. The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification. Technical Report MPI-I-98-2-005, Max-Planck-Institut für Informatik, February 1998.

1997

• M. Veanes. The undecidability of simultaneous rigid E-unification with two variables. 5th Kurt Gödel Colloquium KGC'97, LNCS 1289 pp. 305-318.
• Y. Gurevich and M. Veanes. Some undecidable problems related to the Herbrand theorem. UPMAIL Technical Report 138, Uppsala University, Computing Science Department, 1997.
• A. Degtyarev, Yu. Gurevich, P. Narendran, M. Veanes, and A. Voronkov. The decidability of simultaneous rigid E-unification with one variable. UPMAIL Technical Report 139, Uppsala University, Computing Science Department, 1997.
• M. Veanes. On computational complexity of basic decision problems of finite tree automata. UPMAIL Technical Report 133, Uppsala University, Computing Science Department, January 1997.

1996

• M. Veanes. Uniform representation of recursively enumerable sets with simultaneous rigid E-unification (extended abstract). Proc. 10th International Workshop on Unification (UNIF'96), Munich University, CIS-Bericht-96-91, pp. 7-15, 1996.
• M. Veanes. Uniform representation of recursively enumerable sets with simultaneous rigid E-unification. UPMAIL Technical Report 126, Uppsala University, Computing Science Department, July 1996.
• M. Veanes and J. Barklund. Construction of natural cycletrees. Information Processing Letters, 60:313-318, 1996.
• M. Veanes and J. Barklund. Natural cycletrees: Flexible interconnection graphs. Journal of Parallel and Distributed Computing, 33(1):44-54, 1996.
• M. Veanes and J. Barklund. On the number of edges in cycletrees. Information Processing Letters, 57:225-229, 1996.

1995

• J. Barklund, K. Boberg, P. Dell'Acqua and M. Veanes. Metaprogramming with Theory Systems. UPMAIL Technical Report 106, Uppsala University, Computing Science Department, 1995.
• M. Veanes and J. Barklund. Cycletrees: flexible interconnection graphs for parallel computing. UPMAIL Technical Report 97, Uppsala University, Computing Science Department, 1995.

• M. Veanes. On Simultaneous Rigid E-Unification. Doctoral thesis, Computing Science Department, Uppsala University, 1997. Uppsala Theses in Computing Science No. 29/97. (PDF file)
  If you are interested in an original hardcopy, drop me an email and I'll send you one!
• M. Veanes. Cycletrees: a Novel Class of Interconnection Graphs. Licentiate thesis (Masters with Honors), Computing Science Department, Uppsala University, 1993. Uppsala Theses in Computing Science No. 17/93.

Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte: Model-Based Software Testing and Analysis with C#, Cambridge University Press, 2008.

In the M3 project we investigate various foundational questions and decision problems related to reasoning about high-level models that may use rich background universes or combinations of different theories. This project is my main research focus.

NModel is an open source codeplex project. It is a model based testing framework for C# and provides software support for the above book. The main coordinator of the NModel project is Jonathan Jacky.

AsmL is an executable specification language developed in the FSE group and is based on the theory of Abstract State Machines invented by Yuri Gurevich.

This site was last updated 10/20/08