I'm a computer scientist specialized in the areas of
Since 2022, I have been working for Signaloid; first as a consultant, and now as Quality Assurance Lead. Between 2016 and 2021, I was a research group leader at MPI-SWS. 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.
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. These applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We are looking at a programming model which brings together software and hardware. This project has multiple parts. With PGCD we are working on an unifying programming model combining message-passing concurrency and control code which interacts with the physical world. With MPerl we look at how progress in rapid manufacturing tools like 3D printers influence the way we write code for robotic systems. More precisely, we are working generating control code from parametric description of robotic designs.
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.
A list of the various tools that I developed and participated in the development. Most of these tools are academic prototypes and are not maintained anymore.