Overview

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. FSE is part of RiSE, Research in Software Engineering at Microsoft Research in Redmond.

Projects

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.

DKAL: Distributed Authentication Language. DKAL In an increasingly interconnected world authorization policies grow more involved. Rights depend upon external credentials that may rely upon other credentials. DKAL is an expressive high-level autorization language for distributed systems. The intention is to handle access control in a secure, uniform and comprehensible way amenable to analysis, to facilitate policies that are more modular and thus more stable in the changing environment. DKAL allows one to write high-levl policy rules in a human-readable form. The result declarative policy serves as a base, a legal manifesto of sorts, from which specific permissions are defined.

Logic and Foundations. These days not too many people worry about foundations of mathematics which is a compliment of sorts: the foundations are solid. Computer science is younger, and its foundations are still work in progress. Logic and Foundations is really a meta-project. Here are some parts in alphabetical order: Abstract State Machines and Behavioral Computation Theory; Database theory; Decision problems and Computational Complexity; Logic and Model Theory, in particular Finite Model Theory; Security; Specification and Testing.

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.

M3: Model theory, Model generation and Models. M3 project investigates various foundational questions and studies decision problems related to reasoning about high-level models that use rich data types or combinations of different theories.

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.

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.

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

Members: Nikolaj Bjorner, Yuri Gurevich, Ethan Jackson, Peli de Halleux, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
Alumni: Lev Nachmanson, Colin Campbell, Wolfgang Grieskamp
Visitors 2008: Andrei Voronkov, Grigore Rosu
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

Papers are listed in the member and project pages.

Academic involvement

WING 2009, CADE 2009, CAV 2009, LPAR 2008, IJCAR 2008, ISSTA 2008, MBT 2008, 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.

Jobs

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