I am an Assistant Professor in the NYU Computer Science Department and a member of the Analysis of Computer Systems Group. I received my doctorate in Computer Science from the University of Freiburg, Germany (2009). Before joining NYU, I held post-doctoral positions at École Polytechnique Fédérale de Lausanne, Switzerland and at the Institute of Science and Technology Austria.

See also my curriculum vitae.

Research

My research focuses on program analysis and verification, automated deduction, concurrent software, and software productivity.

Recent Publications

New Automating Separation Logic using SMT with Ruzica Piskac and Damien Zufferey
To appear in Proceedings of CAV, 2013. [pdf] [pdf-extended]
New Structural Counter Abstraction with Kshitij Bansal, Eric Koskinen, and Damien Zufferey
In Proceedings of TACAS, 2013. [pdf] [pdf-extended]
New Complete Instantiation-Based Interpolation with Nishant Totla
In Proceedings of POPL, 2013. [pdf] [pdf-extended]
New Flow-Sensitive Fault Localization with Jürgen Christ, Evren Ermis, and Martin Schäf
In Proceedings of VMCAI, 2013. [pdf]
Error Invariants with Evren Ermis and Martin Schäf
In Proceedings of FM, 2012. [pdf]
Ideal Abstractions for Well-Structured Transition Systems with Damien Zufferey and Thomas A. Henzinger
In Proceedings of VMCAI, 2012. [pdf]
Deciding Functional Lists with Sublist Sets with Marco Muñiz and Viktor Kuncak
In Proceedings of VSTTE, 2012. [pdf] [pdf-extended]

As a byproduct of my research projects, I have developed and contributed to a number of tools.

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.

Program committee member: