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

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/

People

Publications

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

Downloads

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

Videos

Link description

In Systems We Trust

Date

February 6, 2014

Speakers

Joe Hendrix

Affiliation

Galois

Link description

Fairness in Theorem Proving

Date

June 26, 2013

Speakers

Maria Paola Bonacina

Affiliation

Universita degli Studi di Verona

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

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

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

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

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

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

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

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

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

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

Link description

Causality Checking

Date

September 10, 2012

Speakers

Stefan Leue

Affiliation

University of Konstanz

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…

PROMOTO 2014—2nd Workshop on Programming for Mobile and Touch

Portland, OR, United States | October 2014

The second PROMOTO Workshop was held in Portland, Oregon, as part of SPLASH/OOPSLA 2014, October 20–24, 2014. Programming with Mobile and Touch (PROMOTO) is a forum for embracing the new realities of always-connected and/or touch-enabled devices. Topics under discussion included cross-platform computing, cloud computing, social applications, privacy, and security. The challenges of new types of devices, such as large screens or gadgets with no screens, are very important.   Theme and goals Today, easy-to-use mobile…

SEIF Day 2014

Redmond, WA, US | July 2014

The annual Software Engineering Innovation Foundation (SEIF) Day brought together SEIF winners, influential software engineering researchers, and researchers from Microsoft Research to present and discuss existing software engineering projects being pursued by the SEIF community, and future directions in software engineering research.       Organization

SEIF Day 2012

Redmond, WA, US | July 2012

The annual Software Engineering Innovation Foundation (SEIF) Workshop brings together SEIF winners, influential software engineering researchers, and researchers from Microsoft Research to present and discuss existing software engineering projects being pursued by the SEIF community, and future directions of software engineering research. 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…

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

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, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year. Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We…

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 code. They offer systematic testing capabilities that exhaustively (in the limit) tests all possible executions of the program, weeding out even hard-to-find concurrency bugs. P is a (domain-specific) programming language for modeling and specifying protocols…

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 supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness. IVy is joint work with the following people: Oded Padon, Tel Aviv University Aurojit…

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 to see the exact sequence of statements and program values leading to an error. This project is being developed, in conjunction with partners in DevDiv, as part of the ChakraCore JavaScript engine (available on GitHub). Preview releases…

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 is on GitHub: (https://github.com/klipto/uncertainty)

Automata

Established: November 1, 2015

github.com/AutomataDotNet

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 what you are doing. Sign up here. Announcing CHESE 2016 The 2nd Int’l Code Hunt Workshop on Educational Software Engineering (CHESE 2016) will be held in Seattle, WA, on November 18 in conjunction with FSE…

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 year old child in Year 7 or equivalent across the UK, for free. “The simple truth is, being a maker matters. Real computing, doing not just consuming, will drive a creative revolution in this country.…

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 as early as possible to predict disease spread and plan responses. Yet early data is very difficult to obtain, because it must be proactively collected from potential disease sources in the environment. Researchers estimate between…

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 with test cases only, no specification. Players have to first work out the pattern and then code the answer. Code Hunt has been used by over 350,000 players as of August 2016. Data from the…

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 [Slides] [Video] (after Bishop) Hint generation in Code Hunt  Daniel Perelman [Slides] [Video] A system for C programming  Amey Karkare [Slides] [Video] Semantic Clustering of Student Solutions at Scale Rishabh Singh [Video] (after Karkare) Automatic…

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 assertion checking for any developer. Technically, this translates to finding precise interprocedural defect traces of assertion violations in open programs with under constrained environment (inputs and external methods). The philosophy of AV is to provide…

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 active area of research in static analysis, verification, and partial evaluation. This is exciting as advances in these fields can translate to novel parallel algorithms for sequential computation.

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 create virtual classrooms, customize existing courses, and publish new learning material including learning games. Try it out on the web Go to www.pex4fun.com, and click Learn to start tutorials.

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 and fixed number of context switches. Corral also supports the Duality extension for constructing inductive proofs of correctness of programs. Corral powers Microsoft's Static Driver Verifier tool. This work has received several…

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. This can help avoid copyright or plagiarism issues and help generate personalized workflows. This project develops technologies for problem generation in various subject domains including math, logic, and even language learning. Team This is an…

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 the minimum time required for a typical source code change to move from changed sources via compilation and unit testing to deployed binaries. See projects CloudBuild, MSBuild vNext, and CloudStore. TSE provides additional engineering services…

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 having a small language core with a familiar JavaScript like syntax. The Koka project tries to see if effect inference can be used on larger scale programming. The language is strict (as in ML), but…

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 as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of manual proofs.

Jennisys

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 the public interface and the given data-structure description. Source and Tool Jennisys is available as open source in the Boogie source repository, in the Jennisys directory.  It is written in F# and it makes use…

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.

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.

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 similar to regular apps. Any TouchDevelop user can install, run, edit, publish scripts. You can share scripts with other people by publishing them to the TouchDevelop script bazaar, or by submitting them as an app…

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 Phone! Our good friends from Channel 9 helped us to re-record this movie.     What other people say Social Times: Microsoft Research TouchStudio Makes Windows Phone a Game Changing Platform: Prepare to be Amazed Geek Wire:…

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 properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications…

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 even if those tasks access the same data and may exhibit read-write or write-write conflicts. To find out more about the basic idea and how it works: Read our OOPSLA 2010 paper (links for all publications…

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 that match or don't match the same way as the secret regex. The game uses the ASCII range of characters, i.e. characters from code 0 to 127 and displays various automata associated to the regexes.

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?   Abstract JavaScript is widely used in web-based applications and is increasing popular with developers. So-called ”browser wars” in recent years have focused on JavaScript performance, specifically claiming comparative results based…

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 from Moles, however, so moving from Moles to Fakes will require some modifications to your code. The Moles framework will not be supported in Visual Studio 2012. Read the blog post from Peter Provost about Stubs. Read…

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 Research in Software Engineering (RiSE) group at Microsoft Research, show how a program can be constructed by stepwise refinement. YouTube video Channel9 Movie and Podcasts Chalice Sources [zip]  

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 users in the technology pyramid: (100s of millions of) End Users (people who have access to a computational device but are not expert programmers): Helping them to create small snippets of code for performing repetitive…

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 discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications. Saurabh Srivastava, who is leading…

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 a lightweight framework for test stubs in .NET that is entirely based on delegates. Stubs may be used on interfaces, abstract classes or non-sealed classes. Stubs was designed provide a minimal overhead to the Pex white…

Chalice

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 locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice. Because of its permissions model, Chalice has also been used as a test…

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, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers…

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 are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity. VCC is available for non-commercial use, with sources, at our codeplex site.  …

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) and model transformations. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation…

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? Encode a system's intended behavior (its specification) in machine-executable form (as a "model program"). The model program typically does much less than the implementation; it does just enough to capture the relevant states of the…

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 Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes…

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, or by having algorithms that are complicated and have long running-time. It is interesting to consider if we can pay for this hardness by compromising soundness a little bit (and thus benefit by having simpler…

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 before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic computational complexity of programs. It builds over recent advances in static program analysis, which has traditionally been used for checking…

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 and arrays. The main challenge addressed by the tool are (1) tradeoff between expressiveness of the assertion logic and its computational efficiency, (2) generic inference techniques to relieve users of annotation burden for large modules.

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 formulas over some theory and the partial order relationship is the implication relationship (or some refinement of it). Theorem proving community has studied decision procedures for several theories. For performing abstract interpretation over logical formulas…

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 improve testing via runtime checking, enable static contract verification, and documentation generation. Code Contracts is now Open Source! Code Contracts is now an open source project in GitHub. This page is being kept for historical…

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 proving. Some Microsoft projects using our technology: SAGE: hunting for million-dollar security bugs in Microsoft products. Pex: unit testing of .NET managed programs. Yogi: testing and static analysis of Windows device drivers. Vigilante: automatic generation…

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 debugging. CHESS is available for both managed and native programs. News CHESS open source CHESS Tutorial at PLDI 2009 [slides: ppt, pdf] Channel 9 video on CHESS Read the Dr. Dobb's Journal article on CHESS, listen…

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 Extensions. This power tool includes a server-side extension to IIS to add profiling code to your JavaScript web applications, and a Visual Studio add-in to investigate this data with Visual Studio's Performance Explorer.

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 framework is provided with Pex, or can be installed by itself as a Microsoft Visual Studio add-in. NEW: IntelliTest in Visual Studio 2015 is the evolution of Pex. IntelliTest is a feature integrated in Visual…

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 object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.

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 West Coast and Asia. "...it is impossible to predict how a singularity will affect objects in its causal future." - NCSA Cyberia Glossary What's New? The Singularity Research Development Kit (RDK) 2.0 is available for…

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 the Windows Driver Development Kit that uses the SLAM verification engine. "Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very…

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, no matter what source language it is written in. AsmL uses XML and Word for literate specifications. What is AsmL? AsmL is the Abstract State Machine Language. The FSE group develops AsmL. It is an…

Microsoft Research blog

P: A programming language designed for asynchrony, fault-tolerance and uncertainty

P: A programming language designed for asynchrony, fault-tolerance and uncertainty

By Shaz Qadeer, Principal Researcher The complexity of emerging software applications requires new approaches to understanding and then efficiently building, testing and debugging these systems. Today’s software uses cloud resources, is often embedded in devices in the physical world and employs artificial intelligence techniques. These three factors make today’s software systems an order of magnitude more difficult to develop. Often, these modern applications feature asynchrony, which happens when, to improve performance, the requestor of an…

May 2017

Microsoft Research Blog

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 ago: MSR gives you the freedom to explore and expand the bounds of scientific knowledge, as in academia, but with the added challenge to align your scientific pursuits with company problems and to drive for…

January 2017

Microsoft Research Blog

IEEE Computer Society honors Wolfram Schulte for research leadership, contributions to program verification

By George Thomas Jr., Writer, Microsoft Software verification — the crucial process of assuring programs perform as expected — may not be top of mind for most of us. But considering its role in the development of just about anything based on software — which seemingly is nearly everything these days — its importance cannot be understated. And that’s where Wolfram Schulte comes in. In his nearly two decade-long career at Microsoft, Schulte has made…

February 2016

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 a holy grail for computer science for 40 or 50 years,” said Bryan Parno, a Microsoft researcher who is one of the co-authors of a forthcoming paper on the project. The researchers caution that we…

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 data centers can be located, how close to capacity they can operate, and how robust they are to failure. In part, however, this is true because computers are precision machines. They’re hard-wired that way. Ask…

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, Research in Software Engineering (RiSE), headed by Wolfram Schulte, includes a diverse set of topics such as experimental software engineering, human interactions in programming, software reliability, programming-language design and implementation, and theorem proving. He recently…

December 2008

Microsoft Research Blog