Research in Software Engineering (RiSE)

Established: November 24, 2008

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



  • 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



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


Play with RISE tools





















CCI (Common Compiler Infrastructure)

January 2017

CCI provides a rich infrastructure for working with .NET Assemblies: generating them from source, or rewriting them.

    Click the icon to access this download

  • Github


Link description

In Systems We Trust


February 6, 2014


Joe Hendrix



Link description

Fairness in Theorem Proving


June 26, 2013


Maria Paola Bonacina


Universita degli Studi di Verona

Link description

Graph Drawing 2012 Day 3 – Session 4


September 21, 2012


Benjamin Bach, Andrew Suk, Gabor Tardos, and Eric Fusy


INRIA, MIT, School of Computing Science, LIX

Link description

Graph Drawing 2012 Day 3 – Session 3


September 21, 2012


Christopher Auer, Martin Balko, Kathrin Hanauer, Seok-Hee Hong, and Andres J. Ruiz-Vargas


University of Passau, Charles University in Prague, University of Sydney, EPF Lausanne

Link description

Graph Drawing 2012 Day 3 – Session 2


September 21, 2012


Till Tantau, Rahnuma Islam Nishat, William Lenhart, and Csaba Toth


Universität zu Lübeck, University of Victoria, Williams College, University of Calgary

Link description

Graph Drawing 2012 Day 3 – Session 1


September 21, 2012


Andreas Gemsa, Robert Zeranski, Soroush Alamdari, Marc van Kreveld, and Kevin Verbeek


Karlsruhe Institute of Technology (KIT), Friedrich-Schiller-Universität Jena, University of Waterloo, Utrecht University, TU Eindhoven

Link description

Graph Drawing 2012 Day 2 – Session 2


September 20, 2012


Marcus Schaefer, Daniel Archambault, Steven Chaplick, and Chris Muelder


DePaul University, University College Dublin, University of Toronto, U. C. Davis

Link description

Graph Drawing 2012 Day 2 – Session 1


September 20, 2012


David Eppstein, Martin Nöllenburg, Michael Bekos, Michael Kaufmann, and Martin Fink


Univ. of California, Karlsruhe Institute of Technology, University of Tubingen, University of Würzburg

Link description

Graph Drawing 2012 Day 2 – Session – 3


September 20, 2012


Ioannis Tollis, Fabrizio Frati, Debajyoti Mondal, Muhammad Jawaherul Alam, and Roman Prutkin


Univ. of Crete and ICS-FORTH, The University of Sydney, University of Manitoba, University of Arizona, Karlsruhe Institute of Technology

Link description

Graph Drawing 2012 Day 1 – Session 2


September 19, 2012


Ulrik Brandes, Lowell Trott, Till Bruckdorfer, and Marco Di Bartolomeo


University of Konstanz, University of California, Irvine, University of Tubingen, Università Roma Tre

Link description

Graph Drawing 2012 Day 1 – Session 3


September 19, 2012


Karsten Klein, Martin Gronemann, Soroush Alamdari, Emilio Di Giacomo, and Emden Gansner


The University of Sydney, University of Cologne, University of Waterloo, University of Perugia, AT&T Labs - Research

Link description

Graph Drawing 2012 Day 1 – Session 1


September 19, 2012


Adam Sheffer, Joe Fowler, Thomas Blasius, and Quan Nguyen


Tel-Aviv University, University of Arizona, Karlsruhe Institute of Technology (KIT), University of Sydney

Link description

Causality Checking


September 10, 2012


Stefan Leue


University of Konstanz

Link description

Blame for All


August 30, 2011


Philip Wadler


University of Edinburgh


Software Engineering Mix

Bellevue, WA, USA | July 2015

Software Engineering Mix provides a forum for our colleagues from academia to interact directly with Microsoft engineers. The program will feature talks from academics: highlights of published research that is highly relevant for Microsoft and blue sky talks summarizing emerging research areas. In addition, practitioners will give presentations about theoretical and pragmatic engineering challenges they face, perhaps soliciting help from academia. A coffee round table setting will be used to facilitate discussions. This session builds on the success of SEIF Days, which provided a discussion forum about the future of software engineering.

SEIF Day 2014

Redmond, WA, US | July 2014

Venue: Microsoft Conference Center Building 33 16070 NE 36th Way, Redmond, WA 98052 Previous Workshop: SEIF Day 2012

SEIF Day 2012

Redmond, WA, US | July 2012

Software Engineering Innovation Foundation (SEIF) was formed in 2009 with a mission to foster research in software engineering tools, applications, and education. Over the past three years, SEIF has provided funding for research in seminal software engineering areas, data-driven software engineering,…

Latin American Faculty Summit 2011

Cartagena, Colombia | May 2011

Microsoft Research hosted its seventh annual Latin American Faculty Summit in Cartagena, Colombia, May 18 to 20, 2011. This event was organized in partnership with Colciencias. The theme of the 2011 summit was Advancing Computing; Advancing Science. View videos of the presentations from the summit on the Videos tab.


Program Synthesis

Established: January 1, 2010

Introduction Program synthesis is the task of automatically discovering an executable piece of code given user intent expressed using various forms of constraints such as input-output examples, demonstrations, natural language, etc. Program synthesis has direct applications for various classes of…

Random Interpretation (Random Testing + Abstract Interpretation)

Established: December 1, 2008

Randomized Algorithms for Formal Verification Powerpoint Slides on Random Interpretation Introduction A sound and complete program analysis is provably hard. We typically pay a price for the hardness of program analysis in terms of having an incomplete (i.e. conservative) analysis,…

Logical Abstract Interpretation

Established: November 3, 2008

Abstract Interpretation over Logical Formulas Powerpoint Slides on Logical Abstract Interpretation (Lectures given in a graduate class on Static Program Analysis at UCLA and at IISc-Bangalore) Introduction Logical Abstract Interpretation means performing abstract interpretation over abstract domains whose elements are logical…

Angelic Verification

Established: January 1, 2015

Angelic verification (AV) is a project for bringing the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static…

Code Hunt Workshops

Established: February 1, 2015

1st Code Hunt Workshop, Redmond February, 15-16, 2015 Slides and Videos Deep Dive into Pex for Code Hunt Nikolai Tillmann [Slides] [Video] Code Hunt Contest Analytics Judith Bishop [Slides] [Video] Model Counting for Test Coverage in Code Hunt  Willem Visser…


Established: November 1, 2015

Safe asynchronous programming with P and P#

Established: March 15, 2016

We are designing programming languages for building safe and reliable asynchronous systems. The languages are based on the programming idiom of communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of…


Established: March 14, 2016

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness. It also provides a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and…

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle,…

Project Premonition

Established: March 2, 2015

Interested in evaluating Project Premonition technologies and data? Sign up here Project Premonition aims to detect pathogens before they cause outbreaks Emerging infectious diseases such as Zika, Ebola, Chikungunya and MERS are dangerous and unpredictable. Public health organizations need data…

JavaScript Time-Travel Debugger

Established: January 8, 2016

This project is focused on creating a low-overhead Time-Traveling Debugger in the Chakra JavaScript engine (and Node.js). This debugger supports reverse variations of the step forward operations in a debugger to enable a developer to easily reverse program execution time…


Established: January 5, 2016

Uncertainty is a C# library that uses LINQ to let developers easily express probabilistic computations and then inference over those computations. See our recorded Research In Focus talk from the Microsoft Faculty Summit this past year for more information. Uncertain…

The BBC micro:bit and Microsoft

Established: May 28, 2015

Try our Block/JavaScript editor! The BBC and partners, including Microsoft, announce the BBC micro:bit – a pocket-sized, codeable computer that allows children to get creative with technology. Up to 1 million micro:bits will be given to every 11 or 12…

Code Hunt Community

Established: July 17, 2015

Code Hunt is a serious educational game. The Code Hunt community is interested in all aspects of research and development around the game, including analysis of the data and development of the platform. Join the Community Get updates. Tell us…

Code Hunt

Established: February 4, 2015

Code Hunt is a serious gaming platform for coding contests and practicing programming skills. It is based on the symbolic white box execution engine, Pex. Code Hunt is unique as an online coding platform in that each puzzle is presented…


Established: October 17, 2014

Parasail is a novel approach to parallelizing a large class of seemingly sequential applications wherein dependencies are, at runtime, treated as symbolic values. The efficiency of parallelization, then, depends on the efficiency of the symbolic computation, an…


Established: June 6, 2013

Pex4Fun is a browser-based teaching and learning environment targeting teachers and students for introductory to advanced programming or software engineering courses. At the core of the platform is an automated grading engine based on symbolic execution. In Pex4Fun, teachers can…

Corral Program Verifier

Established: May 9, 2013

Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3. It is available open source on GitHub. Corral, by default, does a bounded search up to a recursion depth…

Automated Problem Generation for Education

Established: February 25, 2013

Intelligent Tutoring Systems (ITS) can significantly enhance the educational experience, both in the classroom and online. A key aspect of ITS is the ability to automatically generate problems of a certain difficulty level and that exercise use of certain concepts.…

Tools for Software Engineers

Established: June 29, 2012

The Tools for Software Engineers (TSE) team mission is "Enabling Microsoft to accelerate software development". TSE contributes to and innovates on major parts of Microsoft's engineering system. TSE's current focus is to shorten the continuous integration cycle time which is…


Established: April 13, 2012

Koka is a function-oriented programming language that seperates pure values from side-effecting computations, where the effect of every function is automatically inferred. Koka has many features that help programmers to easily change their data types and code organization correctly, while…


Established: February 7, 2012

Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such…

Software Process

Established: February 7, 2012

Our studies on software process include organizational impact on quality, agile software development, global software development, effort estimation, development branches, and build analysis.


Established: February 7, 2012

This is where programs begin. Jennisys is a programming language that emphasizes clean public interfaces and lets programmers describe the data structures they intend a private implementation to use. Code is underemphasized, and Jennisys attempts to synthesize code automatically from…

Software Reliability

Established: February 7, 2012

This project investigates how factors such as complexity metrics, churn, organizational structure, dependencies, and social networks relate to software defects and failures. This information is used to build prediction models that can help to prioritize tests.


Established: July 20, 2011

Create apps everywhere on all your devices! For Windows Phone and the web. In the TouchDevelop programming environment you write scripts by tapping on the screen. You do not need a separate PC or keyboard. Scripts can perform various tasks…

The F* Project

Established: March 25, 2011

F* is a verification-oriented dialect of ML. For more information, please visit or click on the logo below.


Established: March 15, 2011

This project has been renamed to TouchDevelop. Please visit the new Microsoft Research project website and see what scripts people write on   Videos Watch the Channel 9 video to learn how to Script Your Phone ON Your…

SymDiff: Differential program verifier

Established: October 14, 2010

SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential/relational…

Concurrent Revisions

Established: September 15, 2010

The Revisions project introduces a novel programming model for concurrent, parallel, and distributed applications. It provides programmers with a simple, yet powerful and efficient mechanism (based on mutable snapshots and deterministic conflict resolution) to execute various application tasks in parallel…

Rex – Regular Expression Exploration

Established: March 27, 2010

Rex is a tool that explores .NET regexes and generates members efficiently. Try out Rex in duel mode at! The duel mode is a game where you have to guess a secret (hidden) regex. On each attempt, Rex generates strings…

Moles – Isolation framework for .NET

Established: January 25, 2010

Moles allows to replace any .NET method with a delegate. Moles supports static or non-virtual methods. Moles works well with Pex. The Fakes Framework in Visual Studio 2012 is the next generation of Moles & Stubs. Fakes is different…

The Verification Corner

Established: January 8, 2010

The Verification Corner is a video series on YouTube that explains different concepts of software verification.         Stepwise refinement - 10/8/2010: In this episode, Kuat Yessenov and Rustan Leino, Principal Researcher in the…

JSMeter: Measuring JavaScript Web Applications

Established: March 2, 2010

The goal of JSMeter is to measure the runtime behavior of JavaScript programs. Our ultimate goal is to improve the quality of JavaScript engine implementations. Can you tell the JavaScript benchmark from the Real Web App?   …

Stubs – Lightweight Test Stubs for .NET

Established: March 19, 2009

Stubs is a lightweight framework for .NET that provides test stubs. For interfaces and non-sealed classes, type-safe wrappers are generated that can be easily customized by attaching delegates. Stubs are part of Moles, and work well together with Pex. Stubs is…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative,…


Established: December 23, 2008

Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained…

Boogie: An Intermediate Verification Language

Established: December 10, 2008

Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for…

Model-based Testing with SpecExplorer

Established: December 10, 2008

Spec Explorer is a software development tool for advanced model-based specification and conformance testing.   New Version of Spec Explorer as an extension to Visual Studio is now available: Spec Explorer 2010 What are the core ideas behind Spec Explorer?…

FORMULA – Modeling Foundations

Established: December 10, 2008

FORMULA 2.0: Formal Specifications for Verification and Synthesis Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs)…

VCC: A Verifier for Concurrent C

Established: December 10, 2008

VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs…

VS3 (Verification and Specification using SMT Solvers)

Established: December 1, 2009

SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically…

SPEED (Symbolic Resource Time/Space Bounds Analysis)

Established: December 1, 2008

Introduction Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause…


Established: November 25, 2008

HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists…

Code Contracts

Established: October 28, 2008

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to…

Automated Test Generation (ATG)

Established: October 3, 2008

Overview We are conducting research on automating software testing using (static and dynamic) program analysis with the goal of building testing tools that are automatic, scalable and check many properties. Our work combines program analysis, testing, model checking and theorem…

CHESS: Find and Reproduce Heisenbugs in Concurrent Programs

Established: October 1, 2008

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved…


Established: February 7, 2008

Doloto stands for Download Time Optimizer and is also the Russian word for chisel.    

Ajax View

Established: April 30, 2007

Ajax View enables developer to see and control the behaviors of their web applications on user's desktops.     News April 29, 2009: The technology in Ajax View is now available as a Power Tool: Microsoft Visual Studio AJAX Profiling…

Pex and Moles – Isolation and White box Unit Testing for .NET

Established: February 21, 2007

Pex automatically generates test suites with high code coverage using automated white box analysis. Pex is a Visual Studio add-in for testing .NET Framework applications. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles…


Established: June 11, 2004

Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about…


Established: July 9, 2003

OS and tools for building dependable systems. The Singularity research codebase and design evolved to become the Midori advanced-development OS project. While never reaching commercial release, at one time Midori powered all of Microsoft's natural language search service for the…


Established: November 5, 2001

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in…

AsmL: Abstract State Machine Language

Established: November 2, 2001

AsmL is an industrial-strength executable specification language. It can be used at any stage of the programming process: design, coding, or testing. It is fully integrated into the Microsoft .NET environment: AsmL models can interoperate with any other .NET assembly,…


Microsoft Research and the industrial research cycle

A personal view By Thomas Ball, Research Manager, Research in Software Engineering (RiSE) group, Microsoft Research The industrial research cycle Here is what I have told new hires of Microsoft Research (MSR) since I became a manager some 14 years…

January 2017

Microsoft Research Blog

Microsoft researchers explore a practical way to build bug-free software

Posted by Allison Linn Microsoft researchers have figured out a way to build software systems spanning many computers that can be proven free of bugs, a significant feat in the decades-long quest to create perfect software. “Program verification has been…

October 2015

Microsoft Research Blog

Energy-Efficiency Work Reaps Rewards

By Rob Knies, Managing Editor, Microsoft Research These days, more than ever, it’s important for computing to be energy-efficient. Particularly in data centers, energy requirements represent a significant portion of operational costs, and power and cooling needs help dictate where…

August 2009

Microsoft Research Blog

New Area in Microsoft Research: Looking for a RiSE in Developer Productivity

By Rob Knies, Managing Editor, Microsoft Research In the summer of 2008, the leadership at Microsoft Research Redmond reorganized an existing set of research groups with a refreshed, more encompassing mandate: reinventing all aspects of software development. The revamped area,…

December 2008

Microsoft Research Blog