Share this page
Share this page E-mail this page Print this page RSS feeds
Home > People > Wolfram Schulte

Wolfram Schulte

RESEARCH AREA MANAGER

Microsoft Research
One Microsoft Way
Building: B99, Room 2234
Redmond, WA 98052-6399, USA
Email : schulte at microsoft dot com
Phone : +1 425 703-4641
Fax : +1 425 936-7329
http://research.microsoft.com/~schulte/
How to get to MSR, Redmond 

What I do

I'm a principal researcher at Microsoft Research Redmond and the founding manager of that lab's Research in Software Engineering area. I joined Microsoft Research in 1999 as an individual researcher.

My research concerns the practical application of formal methods. At Microsoft, I have co-lead research projects on on software analysis and verification (the Spec# and VCC projects), on software testing (the Pex, SpecExplorer, and nModel projects), on programing language and runtime system design (the AsmL, , and TPL projects), and, lately, on model-driven engineering of applications for embedded systems and the cloud (the Formula and BAM project).

Before joining Microsoft Research, I worked at the University of Ulm (1993-1999), at sd&m, a German software company (1992-1993), and at the Technical University Berlin (1987-1992).

I live in Bellevue, Wash., with my wife Rita, and my two children. In my spare time, I enjoy the beautiful outdoors of the cascades.

Publications

2009

Ernie Cohen, Michał Moskal, Wolfram Schulte, and Stephan Tobies, A Precise Yet Efficient Memory Model For C, Elsevier , May 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

Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies, A Practical Verification Methodology for Concurrent Programs, no. MSR-TR-2009-15, February 2009

Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, and Wolfram Schulte, Specifying and Composing Non-functional Requirements in Model-Based Development, in Proceedings of the 8th International Conference on Software Composition, 2009

Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Under Review, 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

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

Margus Veanes and Wolfram Schulte, Protocol Modeling with Model Program Composition, in FORTE'08, Springer Verlag, June 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

Ethan K. Jackson, Wolfram Schulte, and Janos Sztipanovits, The Power of Rich Syntax for Model-based Development, 2008

Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte, VCC: Contract-based Modular Verification of Concurrent C, 2008

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

Stefan Maus, Michal Moskal, and Wolfram Schulte, Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving, in AMAST, Springer, 2008

Bart Jacobs 0002, Frank Piessens, Jan Smans, K. Rustan M. Leino, and Wolfram Schulte, A programming model for concurrent object-oriented programs, in ACM Trans. Program. Lang. Syst., vol. 31, no. 1, Association for Computing Machinery, Inc., 2008

Daan Leijen and Wolfram Schulte, The Design of a Task Parallel Library, 2008

Ethan K. Jackson and Wolfram Schulte, Synthesis of Cloud Applications using Logic Programming: BAM!, 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

Jan Smans, Bart Jacobs 0002, Frank Piessens, and Wolfram Schulte, An Automatic Verifier for Java-Like Programs Based on Dynamic Frames, in FASE, Springer, 2008

Ethan K. Jackson and Wolfram Schulte, Compositional Modeling for Data-Centric Business Applications, in Software Composition, Springer, 2008

Ethan K. Jackson and Wolfram Schulte, Model Generation for Horn Logic with Stratified Negation, in FORTE, Springer, 2008

K. Rustan M. Leino, Michal Moskal, and Wolfram Schulte, Verification Condition Splitting, 2008

Matko Botincan, Matthew Parkinson, and Wolfram Schulte, Verifying C Using Separation Logic, 2008

2007

Margus Veanes, Colin Campbell, and Wolfram Schulte, Composition of Model Programs, in FORTE, Springer Verlag, June 2007

K. Rustan M. Leino and Wolfram Schulte, Using History Invariants to Verify Observers, in ESOP, Springer, 2007

Margus Veanes, Colin Campbell, and Wolfram Schulte, Parallel and Serial Composition of Model Programs, no. MSR-TR-2007-22, 2007

2006

K. Rustan M. Leino and Wolfram Schulte, Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedings, no. MSR-TR-2006-117, August 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 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, 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

Michael Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun, Allowing State Changes in Specifications, in ETRICS, Springer, 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

Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte, Safe Concurrency for Aggregate Objects with Invariants: Soundness Proof, no. MSR-TR-2005-85, June 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

Gavin M. Bierman, Erik Meijer, and Wolfram Schulte, The Essence of Data Access in Comega, in ECOOP, Springer, 2005

Dean Rosenzweig, Davor Runje, and Wolfram Schulte, Model-Based Testing of Cryptographic Protocols, in TGC, Springer, 2005

Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann, Online testing with model programs, in ESEC/SIGSOFT FSE, ACM, 2005

Yuri Gurevich, Benjamin Rossman, and Wolfram Schulte, Semantic essence of AsmL, in Theor. Comput. Sci., vol. 343, no. 3, pp. 370-412, 2005

Bart Jacobs, Frank Piessens, K. Rustan M. Leino, and Wolfram Schulte, Safe Concurrency for Aggregate Objects with Invariants, in SEFM, IEEE Computer Society, 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

Margus Veanes, Colin Campbell, Wolfram Schulte, and Pushmeet Kohli, On-The-Fly Testing of Reactive Systems, no. MSR-TR-2005-05, January 2005

Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin, Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution, in TACAS, Springer, 2005

2004

K. Rustan M. Leino and Wolfram Schulte, Exception Safety for C#, in SEFM, IEEE Computer Society, 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

2003

Erik Meijer and Wolfram Schulte, Unifying Tables, Objects and Documents, in Proceedings of Declarative Programming in the Context of OO Languages (DP-COOL 2003), August 2003

Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte, Verification of Object-Oriented Programs With Invariants, in Formal Techniques for Java-like Programs (FTfJP), July 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

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

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

2002

Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Generating finite state machines from abstract state machines, in ISSTA 2002, July 2002

2001

Mike Barnett and Wolfram Schulte, Spying on Components: A Runtime Verification Technique, in Workshop on Specification and Verification of Component-Based Systems, October 2001

Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Toward Industrial Strength Abstract State Machines, no. MSR-TR-2001-98, October 2001

Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Conformance Testing with Abstract State Machines, in EUROCAST 2001, February 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