My research interests lie in program analysis and verification, programming languages, distributed systems and automated reasoning.
Until September 2016, I was a Postdoctoral Associate at MIT CSAIL in Martin Rinard's group. I received my PhD in 2013, working under supervision of Thomas A. Henzinger at the Institute of Science and Technology Austria (IST Austria). Prior to that I received a Master in computer science from EPFL in 2009.
For more information, see my complete CV.
Max Planck Institute for Software Systems
315 (3rd floor)
Paul-Ehrlich-Str. 26 (MPI-SWS building)
Google Scholar has citation metrics for my publications.
Fault-tolerant distributed systems play an important role in many critical applications. However, concurrency, uncertain message delays, and the occurrence of faults make those systems hard to design, implement, and verify. PSync is a framework for writing and verifying high-level implementations of fault-tolerant distributed algorithms. PSync is based on the Heard-Of model and provides communication-closed rounds as primitive, which both simplifies the implementation of the fault-tolerant systems, and makes them more amenable to automated verification.
GRASShopper is an experimental verification tool for programs that manipulate dynamically allocated data structures. GRASShopper programs can be annotated with specifications expressed in a decidable specification logic to check functional correctness properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive yet concise specifications.