Participants / Results

Participating Teams

In no particular order:
  1. Bart Jacobs, Jan Smans (VeriFast)
  2. Jean-Christophe Filliâtre, Andrei Paskevich (Why3)
  3. Yannick Moy (GNATprove)
  4. Wojciech Mostowski, Daniel Bruns (KeY)
  5. Valentin Wüstholz, Maria Christakis (Dafny) (student, non-developer team)
  6. Gidon Ernst, Jörg Pfähler (KIV) (student team)
  7. Stefan Blom, Tom van Dijk (ESC/Java2) (non-developer team)
  8. Zheng Cheng, Marie Farrell (Dafny) (student, non-developer team)
  9. Claude Marché, François Bobot (Why3)
  10. Ernie Cohen (VCC)
  11. Nguyen Truong Khanh (Pat)

Awarded Prizes

The main results of the competition are as follows:
  • Best team: Bart Jacobs, Jan Smans (VeriFast)
  • Best student team: Gidon Ernst, Jörg Pfähler (KIV)
  • Distinguished user-assistance tool feature: integration of proving and run-time assertion checking in GNATprove (team member: Yannick Moy)
  • Tool used by most teams: prize shared between Dafny and Why3
  • Best (pre-competition) problem submission: "Optimal Replay" by Ernie Cohen


  1. LCP: 11 submissions, of which 8 were judged as correct and complete, and 2 as correct but not complete.
  2. PrefixSum: 8 submissions, of which one (by team VeriFast) was judged correct and complete.
  3. TreeDel: 7 submissions, of which one (by team VeriFast) was judged correct and complete.


The organizers would like to thank Rustan Leino, Nadia Polikarpova, and Mattias Ulbrich for their feedback and support prior to the competition.