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.

Foundations of Correctness

Software Productivity

Systems at Scale

Education

In the News

Awards

2016

  • 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

2015

2014

Source Code

Code Contracts for .NEThttps://github.com/microsoft/codecontracts
Touch Develophttps://github.com/microsoft/touchdevelop
Automate graph layouthttps://github.com/microsoft/automatic-graph-layout
Lean interactive theorem proverhttps://github.com/leanprover/lean
Z3 automated theorem proverhttps://github.com/z3prover/z3
Symbolic automatahttps://github.com/AutomataDotNet/Automata
Boogie intermediate verification languagehttps://github.com/boogie-org/boogie
P asynchronous event-driven programminghttps://github.com/p-org/P
VCC Concurrent C Verifierhttps://github.com/microsoft/vcc
F* language and verifierhttps://github.com/FStarLang/FStar/
Dafny verification languagehttp://dafny.codeplex.com/
Zing model checkerhttp://zing.codeplex.com/
CHESS concurrency toolhttp://chesstool.codeplex.com/

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

Links

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 www.rise4fun.com

Try a Coding Duel at http://www.codehunt.com/

rise2016-medium

The RiSE team consists of 30+ passionate researchers and developers

People

Play with RISE tools

See www.rise4fun.com

Publications

2017

2016

2015

2014

2013

The Design of Bug Fixes
Emerson Murphy-Hill, Thomas Zimmermann, Christian Bird, Nachiappan Nagappan, Tom Zimmermann, Nachi Nagappan, in Proceedings of the 35th International Conference on Software Engineering (ICSE 2013), IEEE, May 1, 2013, View abstract

2012

Videos

In Systems We Trust Link description

In Systems We Trust

Date

February 6, 2014

Speakers

Joe Hendrix

Affiliation

Galois

Fairness in Theorem Proving Link description

Fairness in Theorem Proving

Date

June 26, 2013

Speakers

Maria Paola Bonacina

Affiliation

Universita degli Studi di Verona

Graph Drawing 2012 Day 3  – Session 4 Link description

Graph Drawing 2012 Day 3 – Session 4

Date

September 21, 2012

Speakers

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

Affiliation

INRIA, MIT, School of Computing Science, LIX

Graph Drawing 2012 Day 3  – Session 3 Link description

Graph Drawing 2012 Day 3 – Session 3

Date

September 21, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 3  – Session 2 Link description

Graph Drawing 2012 Day 3 – Session 2

Date

September 21, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 3  – Session 1 Link description

Graph Drawing 2012 Day 3 – Session 1

Date

September 21, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 2  – Session 2 Link description

Graph Drawing 2012 Day 2 – Session 2

Date

September 20, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 2  – Session 1 Link description

Graph Drawing 2012 Day 2 – Session 1

Date

September 20, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 2  – Session – 3 Link description

Graph Drawing 2012 Day 2 – Session – 3

Date

September 20, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 1 – Session 2 Link description

Graph Drawing 2012 Day 1 – Session 2

Date

September 19, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 1 – Session 3 Link description

Graph Drawing 2012 Day 1 – Session 3

Date

September 19, 2012

Speakers

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

Affiliation

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

Graph Drawing 2012 Day 1 – Session 1 Link description

Graph Drawing 2012 Day 1 – Session 1

Date

September 19, 2012

Speakers

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

Affiliation

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

Causality Checking Link description

Causality Checking

Date

September 10, 2012

Speakers

Stefan Leue

Affiliation

University of Konstanz

Blame for All Link description

Blame for All

Date

August 30, 2011

Speakers

Philip Wadler

Affiliation

University of Edinburgh

Events

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.

Projects

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…

Automata

Established: November 1, 2015

github.com/AutomataDotNet

IVy

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

"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 as early as possible to predict disease spread and plan responses. But, early data is very difficult to…

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…

Uncertainty

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…

Parasail

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…

Pex4Fun

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…

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…

Koka

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…

Duality

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.

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.

TouchDevelop

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 https://fstar-lang.org or click on the logo below.

TouchStudio

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 touchdevelop.com.   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 http://rise4fun.com/rex! 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,…

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…

HAVOC

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…

Doloto

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…

Spec#

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…

Singularity

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…

SLAM

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,…

Posts

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