Damien Zufferey

I'm a computer scientist specialized in the areas of

  • program analysis and verification,
  • programming languages and session types,
  • distributed, embedded, and cyber-physical systems.
I focus on developing programming abstractions designed that are amenable to automated verification, i.e., the automatic analysis of software to find mathematical proofs showing the code meets its specification.

I'm currently working as a static analysis scientist at Sonar Source. In 2022, I worked for Signaloid; first as a consultant, and then 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.

E-Mail

CV

Loading recent publications ...
Loading all publications ...

Google Scholar has citation metrics for my publications. The publications are in alphabetical order except when there is a large difference of contribution.

Design, programming, and verification of robotic system

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.

Programming abstraction and verification of fault tolerant distributed algorithms (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.

Verification of heap-manipulating programs (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.

PhD Students

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.

  • PGCD: a programming and verification tool for robotic systems with an emphasis on coordination of multiple robots.
  • MPerl: automating the generation of control code for robotic manipulators.
  • PSync: DSL for fault-tolerant distributed algorithms using partially-synchronous communication-closed rounds.
  • GRASShopper: a verification tool that checks separation logic specifications of heap manipulating programs.
  • Picasso: a PI-CAlculuS-based SOftware analyzer.
  • Automata Tutor: a website for teaching automata theory to undergraduate students. Later the project was taken over by groups at UPenn and UIUC and became http://www.automatatutor.com/
  • CoLT: Concurrency using Lockstep Tool, a tool for model checking of linearizability of concurrent data structure implementations.
  • CSIsat: Constraint Solving for Interpolation, a tool to compute Craig interpolant in QF LA+EUF.
  • Blast: Berkeley Lazy Abstraction Software Verification Tool.

PC co-chair

  • VMCAI 2020, 21st International Conference on Verification, Model Checking, and Abstract Interpretation.
  • NSV 19, 12th International Workshop on Numerical Software Verification.
  • VMW 2017, Verification Mentoring Workshop 2017.

PC member

  • POPL 2021, 48th ACM SIGPLAN Symposium on Principles of Programming Languages.
  • ESOP 2021, 30th European Symposium on Programming.
  • VSTTE 2020, 12th Working Conference on Verified Software: Theories, Tools, and Experiments.
  • APLAS 2019, 17th Asian Symposium on Programming Languages and Systems.
  • SYNASC 2019, 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing.
  • VMCAI 2019, 20th International Conference on Verification, Model Checking, and Abstract Interpretation.
  • Scala 2018, 9th ACM SIGPLAN Symposium on Scala.
  • SAS 2018, 25th Static Analysis Symposium.
  • CAV 2018, 30th International Conference on Computer-Aided Verification.
  • VSTTE 2018, 10th Working Conference on Verified Software: Theories, Tools, and Experiments.
  • PLDI SRC 2018, Student Research Competition at PLDI 2018.
  • TACAS 2018, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
  • CAV 2017, 29th International Conference on Computer-Aided Verification.
  • TAPAS 2017, 8th Workshop on Tools for Automatic Program Analysis.
  • 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.

Awards

Other

`