Damien Zufferey

I am a research group leader at MPI-SWS (Kaiserslautern) since Fall 2016.

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
Paul-Ehrlich-Str. 26
67663 Kaiserslautern


Loading recent publications ...
Loading all 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.


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.

  • CAV 2017, 29th International Conference on Computer-Aided Verification.
  • MEMOCODE 2017, 15th International Conference on Formal Methods and Models for System Design.
  • SYNT 2017, 6th Workshop on Synthesis.
  • SMT 2016, 14th International Workshop on Satisfiability Modulo Theories.
  • GANDALF 2016, 7th International Symposium on Games, Automata, Logics and Formal Verification.
  • SYNT 2016, 5th Workshop on Synthesis.
  • AGERE 2015, ACM SIGPLAN Workshop on Programming based on Actors, Agents, and Decentralized Control 2015.
  • Scala 2015, Scala Symposium 2015.
  • Scala 2014, annual Scala Workshop.