About

I am a member of the Research in Software Engineering group at Microsoft Research. My work aims to improve software reliability by providing programmers with automated tools to analyze their programs. Most of my work has focused on analysis of concurrent software.

Projects

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…

Certification of Symbolic Transaction

Established: May 6, 2015

Logic flaws are prevalent in multiparty cloud services, which cause serious consequences, e.g., an attacker can make purchases without paying, or gets into other people’s accounts without password. For decades, researchers have been advocating formal verification as a solution, but in the real world developers face many major hurdles to do it. We introduce a technology that significantly lowers these hurdles, and show its effectiveness in real-world deployments. Online services enhanced by…

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…

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…

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.

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…

Zing

Established: December 8, 2003

Zing is a flexible and scalable infrastructure for exploring states of concurrent software systems. This infrastructure can be used for validating software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows and Windows Phone. Sources Source code is now available through Codeplex for use and modification/experimentation by research community.

Publications

2016

2015

2014

2013

2012

2011

Delay-bounded scheduling
Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric, in Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Association for Computing Machinery, Inc., January 1, 2011, View abstract, Download PDF
Linear Maps
Shuvendu Lahiri, Shaz Qadeer, David Walker, in ACM SIGPLAN Workshop on Programming Languages meets Program Verification, ACM SIGPLAN, January 1, 2011, View abstract, Download PDF

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

VIS : A System for Verification and Synthesis
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-Vincentelli, Fabio Somenziy, Adnan Aziz, Szu-Tsung Cheng, Stephen Edwards, Sunil Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa, in Proceedings of the 8th International Conference in Computer-Aided Verification, January 1, 1996, View abstract, View external link

Projects