Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Wolfram Schulte
[go: Go Back, main page]
*
Microsoft.com Home|Site Map
Microsoft*

Search:

Wolfram Schulte

. Microsoft Research
One Microsoft Way
Building: Cedar Court 113/4159
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
 		Links
What I do

Since 2006, I'm a research area manager at Microsoft Research in Redmond, Washington, USA. I'm currently managing the following groups:

  • The Foundations of Software Engineering (FSE) group is devoted to improving software development productivity by using modeling, design verification and advanced software testing.
  • The Programming Languages and Methods (PLM) group seeks to improve software development productivity through the design of new programming language features, in conjunction with program verification.
  • The Software Design and Implementation (SDI) investigates issues related to programming language implementation, application development, and software deployment. Our current projects focus on approaches to software error tolerance, real-time and embedded systems, and system configuration.

We're hiring: If you are interested in a full time or internship at MSR, please submit your application here

From 2003-2005 I co-lead research projects for software modeling and verification that include Contracts for C# (the Spec# project), and advanced test-generation and verification tools (the SpecExplorer project and the MUTT project). From 1999-2003 I researched data access integration (The Cω project), and I worked with Abstract State Machines (the AsmL project). I joined Microsoft Research in 1999.

Current Publications

All project relevant publications are on their respective websites. Here are the ones I co-authored. Please respect the publishers copyrights.

The Spec# programming project

  • new, 5 Jan 2007 Using history invariants to verify observers [PDF]
    K. Rustan M. Leino, and Wolfram Schulte.
    To appear in ESOP 2007, Braga, 2007, LNCS TBD.
  • new, 5 Jan 2007 A Verifying Compiler for a Multi-threaded Object-Oriented Language [PDF]
    K. Rustan M. Leino, and Wolfram Schulte.
    To appear in the Marktoberdorf Summer School 2006 Lecture Notes, Marktoberdorf, Springer Verlag.
  • Allowing State Changes in Specifications [PDF]
    In Proc. ETRICS 2006, Freiburg, 2006, LNCS 3995.
  • A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs [PDF]
    Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte.
    To appear in Proc. TV 2006, Seattle.
  • A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs [PDF]
    Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte.
    To appear in Proc. ICFEM 2006, Macau, LNCS 4260.
  • The Spec# Programming System: Challenges and Directions. [PDF]
    Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Faehndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter.
    In Proc. VSTTE 2005, Zuerich
    • .
  • Safe Concurrency for Aggregate Objects with Invariants. [PDF]
    Bart Jacobs, Rustan Leino, and Wolfram Schulte.
    In Proc. SEFM 2005, Koblenz
    • . Revised version of SAVCBS'04 publication.
  • Iterators Revisited: Proof Rules and Implementation [PDF]
    Bart Jacobs, Erik Meijer, Frank Piessens, and Wolfram Schulte
    In Proc. FTFJP 2005, Glasgow.
  • Verification of Multithreaded Object-oriented Programs with Invariants. [PDF]
    Bart Jacobs, K. Rustan M. Leino, and Wolfram Schulte.
    In Proc. SAVCBS'04, Newport.
  • The Spec# Programming System. [PDF]
    Mike. Barnett, K. Rustan M. Leino, and Wolfram Schulte.
    In Proc. CASSIS 2004, Marseille, 2004, LNCS 3362.
  • Exception Safety for C#. [PDF]
    K. Rustan M. Leino, and Wolfram Schulte.
    In Proc. SEFM 2004, Bejing.
  • 99.44% pure: Useful Abstractions in Specifications. [PDF]
    Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun.
    In Proc. FTfJP 2004, Oslo.
  • Verification of Object-Oriented Programs with Invariants. [PDF]
    Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte.
    In Proc. FTfJP 2003, Darmstadt.
    Updated version to appear in Journal of Object Technology. 2004

Spec Explorer: The Spec# modeling and model-based testing project

  • Controllable Combinatorial Coverage in Grammar-based Testing. [PDF]
    Ralf Lämmel, Wolfram Schulte (not a Spec Explorer but a testing paper)
    In Proc. TestCom 2006, LNCS 3964, New York.
  • Model–Based Testing of Cryptographic Protocols. [PDF]
    Dean Rosenzweig, Davor Runje, and Wolfram Schulte
    Appears in TGC 2005.
  • Online Testing with Model Programs. [PDF]
    Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte and Nikolai Tillmann.
    Appears in FSE/ESEC 2005, Lisbon, ACM 2005.
  • Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer [PDF]
    Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes
    MSR-TR 2005-59, Extended Abstract [PDF] (easy read) appears in Formal Methods 2005, LNCS 3582.
  • Strategies for Testing Non-deterministic Systems.  [PDF]
    Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes.
    In ISSTA 2004, International Symposium on Software Testing and Analysis.
  • XRT– Exploring Runtime for .NET: Architecture and Applications [PDF]
    Wolfgang Grieskamp, Nikolai Tillmann, and Wolfram Schulte.
    In Proc. SoftMC 2005

MUTT: Advanced unit testing

  • Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution
    Nikolai Tillmann and Wolfram Schulte.
    IEEE Software, vol. 23, no. 4, pp. 38-47, Jul/Aug, 2006. Earlier version as MSR-TR-2005-153 [PDF], March 2006.
  • Discovering Likely Method Specifications. [PDF]
    Nikolai Tillmann, Feng Chen, and Wolfram Schulte.
    In Proc ICFEM 2006, Macau, LNCS 4260. Earlier version as MSR-TR-2005-146 [PDF], March 2006
  • Parameterized Unit Tests. [PDF]
    Nikolai Tillmann and Wolfram Schulte.
    Proc. of the ESEC/FSE 2005, ACM 2005, earlier as MSR-TR-2005-64, May 2005
  • Symstra: A Framework for Generating Object-Oriented Unit Tests using Symbolic Execution. [PDF]
    Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin.
    In TACAS 2005, LNCS 3440.

Cω: Adding data access (and concurrency) to C#

  • The Essence of Data Access in Cω. [PDF]
    Gavin Bierman, Erik Meijer, and Wolfram Schulte.
    In Proc. 19th ECOOP 2005. LNCS 3586. July 2005.
  • Programming with Rectangles, Triangles, and Circles. [PDF]
    Gavin Bierman, Erik Meijer, and Wolfram Schulte.
    In Proc. XML 2003.
  • Unifying Tables, Objects, and Documents. [PDF]
    Erik Meijer, Wolfram Schulte, and Gavin Bierman.
    In Proc. DP-COOL 2003. vol. 27 of John von Neumann Institute of Computing, also to appear in a vol. of LNCS 2005.)
Brief Bio
  • Here is a brief biography, suitable for seminar announcements and suchlike.

    Since 2006 Wolfram Schulte has been a research area manager for the Foundations of Software Engineering (FSE) group, the Programming Language and Methods (PLM) group, and the Software Design and Implmentation (SDI) group at Microsoft Research in Redmond, Washington, USA. The research of these groups tries to improve software development productivity through rigorous software design, design verification, new programming language features in conjunction with program verification, advanced test generation, and new programming language implementations for sequential, parallel and embedded hardware. In principle, Wolfram's research concerns the practical application of formal techniques. He has published a variety of papers in the areas of language design, verification, testing, program derivation and compilation. Before joining Microsoft Research in 1999, Wolfram 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).
Other Publications

On Abstract State Machines and Testing

  • Semantic Essence of AsmL. [PDF]
    Yuri Gurevich, Benjamin Rossman, Wolfram Schulte.
    In: Theoretical Computer Science. Vol. 343, issue 3, pages 370-412, 2005. Earlier as Microsoft Research Technical Report. MSR-TR-2004-27
  • Generating Finite State Machines from Abstract State Machines. [PDF]
    Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes.
    In ISSTA 2002, International Symposium on Software Testing and Analysis, July 2002.
  • Towards a Tool Environment for Model-Based Testing with AsmL. [PDF]
    Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes.
    In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES 2003), 2003.
  • Validating Use Cases with the AsmL Test Tool. [PDF]
    Mike Barnett, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes.
    In QSIC 2003: Proc. of the Third International Conference on Quality Software, 2003.
  • Runtime Verification of .NET Contracts. [PDF]
    Mike Barnett, and Wolfram Schulte.
    Elsevier Journal of Systems and Software, vol. 65, no. 3, pp. 199-208, 2003. Extended version MSR-TR-2002-38 Contracts, Components, and their Runtime Verification on the .NET Platform.
  • The ABCs of Specification: AsmL, Behavior, and Components [PDF]
    Mike Barnett, and Wolfram Schulte.
    Informatica, vol. 25, no. 4, pp. 517-526, November 2001.
  • Spying on Components: A Runtime Verification Technique. [PDF]
    Mike Barnett, and Wolfram Schulte.
    In Proc. SAVCBS 2002

On Java Formalizations (Prior to Microsoft)

  • A Practical Method for Specification and Analysis of Exception Handling - A Java/JVM Case Study. [available via IEEE]
    Egon Boerger, and Wolfram Schulte.
    In IEEE Transactions on Software Engineering, vol. 26, Issue 9 pp. 872 - 887, 2000.
  • High-Integrity Compilation and Secure Execution of Java. [PDF]
    Wolfram Schulte.
    Habilitation, Univerity of Ulm, 2000.
  • Programmer Friendly Modular Definition of the Semantics of Java. [PDF]
    Egon Boerger, and Wolfram Schulte.
    In J. Alves-Foss, Formal Semantics of Java, vol 1523 of LNCS, pp. 353-404. Springer, 1999.
  • Investigating Java Concurrency Using Abstract State Machines. [PDF]
    Yuri Gurevich, Wolfram Schulte, and Chuck Wallace.
    In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele (eds.), Abstract State Machines: Theory and Applications, vol. 1912 of LNCS, pp. 151-176. Springer, 2000.
  • Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. [PDF]
    Egon Boerger, and Wolfram Schulte.
    In L. Brim and J. Gruska and J. Zlatuska (eds.), Proc. of the 23rd International Symposium on Mathematical Foundation of Computer Science (MFCS´98), vol. 1450 of LNCS, pp. 17-35, Springer 1998.
  • Initialization Problems for Java. [PDF]
    Egon Boerger, and Wolfram Schulte.
    In Software Concepts & Tools, Vol 20. No 4, 1999.
  • Modular Design for the Java Virtual Machine Architecture. [PDF]
    Egon Boerger, and Wolfram Schulte.
    In Egon Börger (ed.), Architecture Design and Validation Methods, Springer-Verlag, pp. 297-357, 2000.

On Functional, Parallel and Object-Oriented Programming (Prior to Microsoft)

  • Tool Support for the Interactive Derivation of Formally Correct Functional Programs. [PDF]
    Walter Guttmann, Helmuth Partsch, Wolfram Schulte, and Tom Vullinghs.
    Journal of Universal Computer Science, vol. 9, no. 2, 2003.
  • Architecture independent massive parallelization of divide-and-conquer algorithms. [PDF]
    Klaus Achatz, and Wolfram Schulte.
    In Proc. Mathematics of Program Construction, vol. 947 of LNCS, pp. 97-127. Springer, 1995.
  • Massive parallelization of divide-and-conquer algorithms over powerlists. [PDF]
    Klaus Achatz, and Wolfram Schulte.
    Science of Computer Programming, vol. 26, pp. 59 - 78, 1996.
  • Functional Object-oriented Programming with Object-Gofer. [PDF]
    Klaus Achatz, and Wolfram Schulte.
    In Informatik '97: Informatik als Innovationsmotor, Informatik aktuell, Springer 1997.
  • The design of a functional GUI library using constructor classes. [PDF]
    Ton Vullinghs, Wolfram Schulte, and Thilo Schwinn.
    In PSI-96: Perspectives of System Informatics, vol. 1181 of LNCS, pp. 398-408, 1996.
  • Lightweight GUIs for Functional Programming. [PDF]
    T. Vullinghs, D. Tuinman and W. Schulte.
    In Proc. of the Seventh International Symposium on Programming Languages, Implementations, Logics and Programs, pp. 341-356, 1995.
  • Deriving Residual Reference Count Garbage Collectors. [not available online]
    Wolfram Schulte.
    In M. Hermenegildo, J. Penjam (eds.): Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP '94. Madrid, Spain, LNCS, vol. 844, Springer 1994.
  • Effiziente und korrekte übersetzung strikter applikativer Programmiersprachen. [not available online]
    Wolfram Schulte
    Dissertation, TU Berlin, 1992.
  • Generating Portable and Efficient Code for a Strict Applicative Language. [not available online]
    Wolfram Schulte and Wolfgang Grieskamp.
    In J. Darlington, R. Dietrich (eds.), Declarative Programming. Springer, 1992.

This site was last updated 06/28/05