About

I am a Research Software Design Engineer in the Research in Software Engineering (RiSE) group.

I have been with the Microsoft Corporation since July 1995. First, I was a member of the Natural Language Processing group in Microsoft Research, moving to the Foundations of Software Engineering group in the fall of 1999. I am now a member of the Research in Software Engineering (RiSE) group. Before coming to Microsoft, I had been an assistant professor of Computer Science at the University of Idaho for three years. I received my PhD in Computer Science from the University of Texas at Austin in 1992.

Projects

Trill

Established: September 19, 2013

Trill is a high-performance in-memory incremental analytics engine. It can handle both real-time and offline data, and is based on a temporal data and query model. Trill can be used as a streaming engine, a lightweight in-memory relational engine, and…

Tempe

Established: September 12, 2013

Tempe is a web service for exploratory data analysis. Below are images of the notebook pages mentioned in our submission to ICSE 2014.

User Experience with Big Data

Big data analytics requires new workflows: high latency queries, massively-parallel code, and cloud computing infrastructures all make handling a big dataset different (and harder) than working on a local machine. We are exploring user experiences for analysts, and thinking about…

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…

Publications

2016

2015

2014

2013

2012

2011

2010

2009

2008

2006

2005

2004

2003

2002

2001

2000

Projects

Other

What I Do

  • Tempe: An environment for doing interactive data analytics. Check out our video! And there’s a blog post describing how Trill and Tempe are being used.
  • Trill: A streaming query processor. It is the fastest in the world. Seriously.
  • Cluster Changes: Improving the process of code review. See our paper “Helping Developers Help Themselves” at ICSE 2015.

What I Did

  • Code Contracts: a language-agnostic way to express specifications in any .NET language. Specifications include method preconditions, postconditions, and object invariants. Code Contracts capture programmer intentions about how methods and data are to be used. You can install the tools from the VS Gallery. And now it has been open-sourced and available at GitHub.
  • CCI: The Common Compiler Infrastructure is the framework to use if you are doing anything related to .NET binaries, either creating them from scratch, modifying existing ones, or just mining them for information. It is open-source and available at CodePlex.
  • ILMerge: a static linker for .NET assemblies.
  • Spec#: an experimental extension to C# that adds contract features such as method pre- and postconditions and object invariants. It also has a non-null type system. The Spec# compiler emits run-time checks that enforce the contracts and the Spec# program verifier uses theorem-proving technology to statically check the consistency between a program and its contracts. Spec# helps programmers write correct software and makes explicit the correct usage of APIs for clients. It is integrated into Visual Studio .NET. It is available as an open source project.