My main area of research is program specification, analysis, testing, and verification.
I am leading the Pex project, in which I develop together with Peli de Halleux a framework for runtime verification and automatic test case generation for .NET applications based on parameterized unit testing and dynamic symbolic execution.
Previously I worked on AsmL, an executable modeling language that comes with a compiler and a test generation tool, and the Spec Explorer 2004 model-based testing tool. Together with Wolfgang Grieskamp I developed XRT, a concrete/symbolic state exploration engine and software model-checker for .NET code. Spec Explorer 2007 is based on this engine, which is now productized internally by the Protocol Engineering Team at Microsoft to facilitate quality assurance of protocol documentation (link).
Before coming to Microsoft Research, I was involved in the development of a school management system in Germany.
2009
- Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann, Symbolic Query Exploration, in ICFEM'09, Springer Verlag, December 2009
- Margus Veanes, Peli de Halleux, and Nikolai Tillmann, Rex: Symbolic Regular Expression Explorer, no. MSR-TR-2009-137, October 2009
- Suresh Thummalapenta, Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte, MSeqGen: Object-Oriented Unit-Test Generation via Mining Source Code, in Proc. 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2009), Association for Computing Machinery, Inc., August 2009
- Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte, Fitness-Guided Path Exploration in Dynamic Symbolic Execution, in Proc. the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2009), IEEE, June 2009
- Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann, Symbolic Query Exploration, no. MSR-TR-2009-65, May 2009
- Madhuri R Marri, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte, An Empirical Study of Testing File-System-Dependent Software with Mock Objects, in Proc. 4th International Workshop on Automation of Software Test (AST 2009), Business and Industry Case Studies, IEEE Computer Society, May 2009
- Kunal Taneja, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte, Guided Path Exploration for Regression Test Generation, in Proc. 31th International Conference on Software Engineering (ICSE 2009), IEEE, May 2009
- Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009) , IEEE, May 2009
- Soonho Kong, Nikolai Tillmann, and Jonathan de Halleux, Automated Testing of Environment-Dependent Programs - A Case Study of Modeling the File System for Pex, in Proc. 6th International Conference on Information Technology: New Generations (ITNG'09), IEEE, April 2009
- Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte, Mutation Analysis of Parameterized Unit Tests, in Proc. International Conference on Software Testing, Verification and Validation Workshops, 2009. ICSTW '09., IEEE, April 2009
- Dries Vanoverberghe, Nikolai Tillmann, and Frank Piessens, Test Input Generation for Programs with Pointers, in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Springer Verlag, March 2009
- Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov, Path Feasibility Analysis for String-Manipulating Programs, in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Springer Verlag, 2009
2008
- Patrice Godefroid, Peli de Halleux, Michael Y. Levin, Aditya V. Nori, Sriram K. Rajamani, Wolfram Schulte, and Nikolai Tillmann, Automated Software Testing Using Program Analysis, in IEEE Software: Special Issue on Software Development Tools, IEEE Computer Society, October 2008
- Nikolaj Bjorner, Nikolai Tillmann, and Andrei Voronkov, Path Feasibility Analysis for String-Manipulating Programs, no. MSR-TR-2008-153, October 2008
- Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte, Fitness-Guided Path Exploration in Dynamic Symbolic Execution, no. MSR-TR-2008-123, September 2008
- Nikolai Tillmann and Jonathan de Halleux, Pex - White Box Test Generation for .NET, in Proc. of Tests and Proofs (TAP'08), Springer Verlag, Prato, Italy, April 2008
- Jonathan de Halleux and Nikolai Tillmann, Parameterized Unit Testing with Pex (Tutorial), in Proc. of Tests and Proofs (TAP'08), Springer Verlag, Prato, Italy, April 2008
- Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis, DySy: Dynamic Symbolic Execution for Invariant Inference, in ICSE '08: Proceedings of the 30th international conference on Software engineering, Association for Computing Machinery, Inc., New York, NY, USA, 2008
- Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, and Nikolai Tillmann, Using Dynamic Symbolic Execution to Improve Deductive Verification, in Proc. 15th International SPIN Workshop, Springer Verlag, 2008
- Nikolai Tillmann and Jonathan de Halleux, White-box testing of behavioral web service contracts with Pex, in TAV-WEB '08: Proceedings of the 2008 workshop on Testing, analysis, and verification of web services and applications, Association for Computing Machinery, Inc., New York, NY, USA, 2008
- Saswat Anand, Patrice Godefroid, and Nikolai Tillmann, Demand-Driven Compositional Symbolic Execution, in Proc. International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008, Springer Verlag, 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
- Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis, DySy: Dynamic Symbolic Execution for Invariant Inference, no. MSR-TR-2007-151, November 2007
- Saswat Anand, Patrice Godefroid, and Nikolai Tillmann, Demand-Driven Compositional Symbolic Execution, no. MSR-TR-2007-138, October 2007
- Nicolas Kicillof, Wolfgang Grieskamp, Nikolai Tillmann, and Victor Braberman, Achieving both model and code coverage with automated gray-box testing, in A-MOST '07: Proceedings of the 3rd international workshop on Advances in model-based testing, Association for Computing Machinery, Inc., New York, NY, USA, 2007
2006
- Nikolai Tillmann and Wolfram Schulte, Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution, in IEEE Software, vol. 23, no. 4, pp. 38-47, IEEE, July 2006
- Nikolai Tillmann, Feng Chen, and Wolfram Schulte, Discovering Likely Method Specifications, no. MSR-TR-2005-146, March 2006
- Wolfgang Grieskamp, Nikolai Tillmann, and Nicolas Kicillof, Action Machines: a Framework for Encoding and Composing Partial Behaviors, no. MSR-TR-2006-11, February 2006
- Nikolai Tillmann, Feng Chen, and Wolfram Schulte, Discovering Likely Method Specifications, in Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM’06), LNCS , Springer Verlag, 2006
- Wolfgang Grieskamp, Nikolai Tillmann, and Wolfram Schulte, XRT- Exploring Runtime for .NET Architecture and Applications, in Electr. Notes Theor. Comput. Sci., vol. 144, no. 3, pp. 3-26, 2006
- Nikolai Tillmann and Wolfram Schulte, Mock-object generation with behavior, in Automated Software Engineering, 2006. ASE '06. 21st IEEE/ACM International Conference on, IEEE Computer Society, 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
- Wolfgang Grieskamp and Nikolai Tillmann, Action Machines - Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation, no. MSR-TR-2005-60, May 2005
- Ana Paiva, Nikolai Tillmann, João C. P. Faria, and Raul F. A. M. Vidal, Modeling and Testing Hierarchical GUIs, in Abstract State Machines, 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann, Online testing with model programs, in ESEC/SIGSOFT FSE, ACM, 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
- Yuri Gurevich and Nikolai Tillmann, Partial updates, in Theor. Comput. Sci., vol. 336, no. 2-3, pp. 311-342, Springer Verlag, 2005
- Ana Paiva, João C. P. Faria, Nikolai Tillmann, and Raul F. A. M. Vidal, A Model-to-Implementation Mapping Tool for Automated Model-Based GUI Testing, in ICFEM, Springer Verlag, 2005
- Nikolai Tillmann and Wolfram Schulte, Parameterized Unit Tests with Unit Meister, in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, Inc., 2005
- Nikolai Tillmann and Wolfram Schulte, Parameterized Unit Tests, in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, Inc., 2005
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
- Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, and Wolfgang Grieskamp, Optimal strategies for testing nondeterministic systems, in ISSTA 2004, ACM, 2004
2003
- Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, and Arthur Watson, Serious Specification for Composing Components, in Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction, May 2003
- Michael Barnett, Wolfram Schulte, and Nikolai Tillmann, Using AsmL for Runtime Verification, in Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Springer Verlag, March 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, Wolfram Schulte, and Nikolai Tillmann, .NET Contracts: Attaching Specifications to Components, in Practical Foundations of Business System Specifications, pp. 83–98, Springer Verlag, 2003
- Yuri Gurevich and Nikolai Tillmann, Partial Updates Exploration II, in Abstract State Machines, Springer Verlag, 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
2001
- Wolfgang Grieskamp, Markus Lepper, Wolfram Schulte, and Nikolai Tillmann, Testable Use Cases in the Abstract State Machine Language, in Proc. 2nd Asia-Pacific Conference on Quality Software (APAQS 2001), IEEE Computer Society, 2001
- Yuri Gurevich and Nikolai Tillmann, Partial Updates: Exploration, in J. UCS, vol. 7, no. 11, pp. 917-951, Springer Verlag, 2001



