Research in Software Engineering (RiSE)

rise_trans_w96pxcoordinates Microsoft’s Research in Software Engineering in Redmond, USA. Our mission is to advance the state of the art in Software Engineering and to bring those advances to Microsoft’s businesses.

 Visit our career page.

Foundations of Correctness

Software Productivity

Systems at Scale


In the News



  • Skolem Award – CADE-21 (2007): Leonardo de Moura and Nikolaj BjørnerEfficient E-Matching for SMT Solvers


  • Mining Software Repositories’ 2016 Most Influential Paper Award for Mining Email Social Networks by Christian Bird, Alex Gourley, Prem Devanbu, Michael Gertz, Anand Swaminathan
  • ICSE 2016 Distinguished Paper Award for Guiding Dynamic Symbolic Execution Toward Unverified Program Executions by Maria Christakis and co-authors
  • Maria Christakis‘s Ph.D. thesis was nominated by ETH for the Gesellschaft für Informatik prize for best dissertation



  • 2014 CAV Award “For the development of partial-order reduction algorithms for efficient state-space exploration of concurrent systems”, Patrice Godefroid, Doron Peled, Antti Valmari, Pierre Wolper
  • ICSE 2014 Most Influential Paper Award, Mining Version Histories to Guide Software Changes, Thomas Zimmermann, Peter Weissgerber, Stephan Diehl and Andreas Zeller
  • “Uncertain: A First-Order Type for Uncertain Data,” J. Bornholt, T. Mytkowicz, and K.S. McKinley, ASPLOS 2014, selected for ACM SIGPLAN Research Highlights, November 2014.
  • FMCAD Best Paper Award. Akash Lal and Shaz Qadeer, A Program Transformation for Faster Goal-Directed Search, in Formal Methods in Computer-Aided Design (FMCAD), FMCAD, October 2014.
  • 2014 ACM SIGMETRICS Test of Time Award, for Kathryn McKinley’s paper “Myths and Realities: The Performance Impact of Garbage Collection” co-authored with Steve Blackburn and Perry Cheng which appeared originally in SIGMETRICS June 2004.
  • FSE 2014 Distinguished Paper: Miltiadis Allamanis, Earl T. Barr, Christian Bird, and Charles Sutton, Learning Natural Coding Conventions
  • FSE 2014 Distinguished Paper: Akask Lal, Shaz Qadeer, Powering the Static Driver Verifier using Corral

Source Code

Code Contracts for .NET
Touch Develop
Automate graph layout
Lean interactive theorem prover
Z3 automated theorem prover
Symbolic automata
Boogie intermediate verification language
P asynchronous event-driven programming
VCC Concurrent C Verifier
F* language and verifier
Dafny verification language
Zing model checker
CHESS concurrency tool

For a complete list of open source projects, see open source.

Past Projects

Asml – Modeling language based on abstract state machines

BAM – Cloud Computing with Models

Cω – The project that started Linq

Daedalus – Improving Data Locality and Scalability

NModel – Model-based Software Testing and Analysis Tool with C#

Ninjaware – Low Overhead Software Monitoring and Analysis

PPP– Preferential Path Profiling

SingularityOS and tools for building dependable systems

SLAM – Software model checking of device drivers

SpecExplorer – Tool for model-based specification and conformance testing

TPL – Task Parallel Library in .NET 4.0

Try RiSE Tools at

Try a Coding Duel at