I am an Assistant Professor in
the NYU Computer Science
Department and a member of
the Analysis of Computer
I received my doctorate in Computer Science from
of Freiburg, Germany (2009). Before joining NYU, I held
at École Polytechnique Fédérale
de Lausanne, Switzerland and at
the Institute of Science and
See also my curriculum vitae.
My research focuses on program analysis and verification, automated deduction, concurrent software, and software productivity.
Complete Heap Verification with Mixed Specifications
with Ruzica Piskac and Damien
To appear in Proceedings of TACAS, 2014. [pdf]
Dynamic Package Interfaces
with Shahram Esmaeilsabzali, Rupak Majumdar, and Damien Zufferey
To appear in Proceedings of FASE, 2014. [pdf]
with Wei Wang and Clark Barrett
In Proceedings of VMCAI, 2014. [pdf]
Explaining Inconsistent Code
with Martin Schäf and Daniel Schwartz-Narbonne
In Proceedings of ESEC/FSE, 2013. [pdf]
Automating Separation Logic using SMT
with Ruzica Piskac and Damien
In Proceedings of CAV, 2013. [pdf] [pdf-extended]
Structural Counter Abstraction
with Kshitij Bansal, Eric Koskinen, and Damien
In Proceedings of TACAS, 2013. [pdf] [pdf-extended]
Complete Instantiation-Based Interpolation
with Nishant Totla
In Proceedings of POPL, 2013. [pdf] [pdf-extended]
Flow-Sensitive Fault Localization
with Jürgen Christ, Evren Ermis, and Martin
In Proceedings of VMCAI, 2013. [pdf]
with Evren Ermis and Martin Schäf
In Proceedings of FM, 2012. [pdf]
Recent Invited Talks
- International Conference on Verification, Model Checking, and Abstract Interpretation, San Diego, CA, USA, January 2014.
- CMACS/AVACS Workshop at CMU, Pittsburgh, PA, USA, November 2013.
- International Workshop on the Future of Debugging, Lugano, Switzerland, July 2013.
- Dependable Software Systems Summer School, NUI Maynooth, Ireland, July 2013.
As a byproduct of my research projects, I have developed and contributed to a number of tools.
- GRASShopper is an experimental verification tool that checks separation logic specifications of programs manipulating dynamically allocated data structures.
- Picasso is a static analyzer for depth-bounded concurrent systems. It has been used to verify properties of non-blocking implementations of concurrent data structures and distributed message passing algorithms with an unbounded number of threads and messages.
- Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints.
- Bohne is a symbolic shape analysis tool. It infers loop invariants of programs manipulating heap-allocated data structures. Bohne is integrated into the Jahob verification system.
- SLAyer is a tool for automatic formal verification of industrial low-level software components. SLAyer is developed at Microsoft Research Cambridge.
- 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. HAVOC is developed at Microsoft Research Redmond.
- Programming Paradigms for Concurrency (graduate), Spring 2014.
- Object-Oriented Programming (undergraduate), Fall 2013.
- Rigorous Software Development (graduate), Spring 2013, Spring 2012.
- Programming Languages (graduate), Fall 2012.
Program committee member: