Damien Zufferey

You should be redirected automatically to my new webpage at http://dzufferey.github.io/.

I am a Postdoctoral Associate at MIT CSAIL in Martin Rinard's group.

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.

MIT CSAIL

Address
MIT CSAIL, 32-G736
32 Vassar St
Cambridge, 02139 MA,
USA

E-Mail
lastname@csail.mit.edu
Loading recent publications ...
Loading all publications ...

Projects

PSync

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

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

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.

  • 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.

Tools

Other

`