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…

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…

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…

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…

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…

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…

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…

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