The goal of the Foundations of Software Engineering (FSE) group at Microsoft Research in Redmond, Wash., is to improve software development productivity by software modeling, design verification, and automated testing.

Spec Explorer: Model-based testing. A model describes the expected behavior of a some aspects of a system under test. The models, describing state transition systems, can be programs themselves or written with diagram notations. The automated verification process algorithmically explores the state space of the model. The results of state exploration become the basis for automatically generated test cases. For more information consult the project website.

Pex: Path-based program exploration. Pex is an intelligent assistant to the programmer. Pex records detailed execution traces of .Net programs. Pex learns the program behavior from the traces, and a constraint solver produces test cases wich uncover different behaviors. By automatically generating unit tests at development time, Pex allows to find bugs early. In addition, Pex suggests to the programmer how to fix the bugs. For more information consult the project website.

AsmL: A modelling language. Earlier we developed the Abstract State Machine Language, based on the theory of abstract state machines, for system modeling, analysis, simulation and conformance testing. The Spec Explorer project builds on this work. In fact, Spec Explorer can be used with AsmL or Spec# as input languages. For more information consult the project website.

Model-based design. We here research formal methods and tool architectures for rapidly constructing domain-specific modeling language and transforming between these using the tool FORMULA (Formal Modeling Using Logic Analysis). Of particular interest is domain-specific abstractions for data-centric business applications (BAM) where constraints topological properties and data integrity are formulated and solved.

Z3: An efficient SMT solver. Z3 is an efficient SMT solver that can be used for symbolic reasoning about software.

Bjørner, Nikolaj

Gurevich, Yuri

de Halleux Peli

Jackson Ethan

Schulte Wolfram

Tillmann Nikolai

Veanes Margus

Manager: Wolfram Schulte
Alumni: Lev Nachmanson, Colin Campbell, Wolfgang Grieskamp
Visitors 2007: Nachum Dershowitz, Tao Xie
Visitors 2006: Jonathan Jacky, Itay Neeman, Andreas R. Blass
Visitors 2005: Dean Rosenzweig, Andreas R. Blass, Daan Leijen, Dave Naumann

Papers are listed in the member and project pages.

FTfJP 2007, FORTE 2007, TESTCOM/FATES 2007, WS-MaTe 2007, IFM 2007, MBT 2007, TAP 2007
ICFEM 2006, FLOC 2006, FATES/RV 2006, LICS 2006, ETRICS 2006
MCSS 2005, RV 2005, FATES 2005, IFM 2005, ICFEM 2005, SAVCBS 2005
ICFEM 2004, The UW/MSR Summer Institute on Software Testing 2004, IFM 2004, SAVCBS 2004.

We're hiring: If you are interested in a full time or internship at MSR, please look at our career page.