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.
Automating Separation Logic using SMT
with Ruzica Piskac and Damien
To appear 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]
Abstractions for Well-Structured Transition Systems
with Damien Zufferey and Thomas A. Henzinger
In Proceedings of VMCAI, 2012. [pdf]
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. HAVOC is developed at Microsoft Research Redmond.
- Object-Oriented Programming (undergraduate), Fall 2013.
- Rigorous Software Development (graduate), Spring 2013, Spring 2012.
- Programming Languages (graduate), Fall 2012.
Program committee member: