I am an Assistant Professor in
the NYU Computer Science
Department and a member of
the Analysis of Computer
Systems Group in the Courant Institute.
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.
Finding Minimum Type Error Sources
with Zvonimir Pavlinovic and Tim King
In Proceedings of OOPSLA (Best Paper Award), 2014. [pdf]
Concolic Fault Abstraction
with Chanseok Oh, Martin Schäf, and Daniel Schwartz-Narbonne
In Proceedings of SCAM, 2014. [pdf]
Separation Logic with Trees and Data
with Ruzica Piskac and Damien Zufferey
In Proceedings of CAV, 2014. [pdf]
Complete Heap Verification with Mixed Specifications
with Ruzica Piskac and Damien
In Proceedings of TACAS, 2014. [pdf]
Dynamic Package Interfaces
with Shahram Esmaeilsabzali, Rupak Majumdar, and Damien Zufferey
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]
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 a verification tool that checks functional correctness of programs manipulating heap-allocated data structures.
- Picasso is a static analyzer for depth-bounded concurrent systems. It has been used to verify properties of non-blocking 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 being 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 being 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: