My research interests lie in program analysis and verification, programming languages, distributed systems, and automated reasoning.
I received my PhD in 2013, working under the 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.
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.
REACT is a domain specific language / library to simplify the programming of robots and remove much of the boiler-plate code. The basic building blocks of REACT are finite state machine (for the control structure), periodic controller, and event handlers. Furthermore, REACT includes a model checker to test safety properties of robotic systems.
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.