RISE Working Group on Formal Methods

Established: February 7, 2012

This is the RISE Formal Methods Working Group















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…



Established: January 1, 2013

(Programming-by-example APIs for extracting structured data from text/log files by examples) The FlashExtract technology (published as a PLDI 2014 paper [pdf |ppt slides |Video |Video 2]) ships as features in Powershell and Azure OMS (Operations Management Suite). FlashExtract powers the ConvertFrom-String cmdlet in Powershell. Here's a Microsoft blogpost that explains this cmdlet. Here are some videos prepared by others to demonstrate this capability: Example-driven parsing Doug Finke's UI Here are some blogposts Powershell PowerShell 5.0…


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.


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…

Flash Fill (Excel feature in Office 2013)

Established: January 1, 2012

Our programming by example work (POPL 2011), also recognized as CACM Research Highlights (CACM 2012), ships as part of the Flash Fill feature in Excel in Office 2013. Here's a small video illustrating this feature. Here's another small video illustrating potential extensions. Here's the inside story of how it came about: Flash Fill Gives Excel a Smart Charge Here are some other videos on FlashFill You-tube: Excel 2013 Flash Fill: 23 Amazing Examples, Excel 2013-…

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.

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…

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…

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…

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…

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