The 4th VerifyThis 2015 Program Verification took place on April 12th,
2015 in London as part of the European Joint Conferences on Theory and
Practice of Software (ETAPS 2015).
The aims of the competition were:
- to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion
- to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others.
During the competition, 14 teams competed on 3 challenges, presented in natural language. Two challenges provided an algorithm in pseudocode, and participants had to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. For the first time, one of the pseudocode algorithms was a concurrent program. The third challenge was to implement and verify several methods on a dancing list data structure.
Prizes were awarded in the following categories:
- Best problem submission Thomas Genet for the “RelaxedPrefix” problem, which was used in the competition
- Tool used by most teams Dafny
- Distinguished user-assistance tool feature Why3 for the lemma library (as demonstrated by its use in the competition), and mCRL2 for a rich specification language in an automated verification tool
- Best student team team KIV - Gidon Ernst & Jörg Pfähler
- Best team team Why3 - Jean-Christophe Filliâtre & Guillaume Melquiond
The competition was organised by Marieke Huisman (U Twente, NL) Vladimir Klebanov (Karlsruhe Institute of Technology, DE) and Rosemary Monahan (NUI Maynooth, IE). The organizers would like to thank Wojciech Mostowski and Radu Grigore for their feedback and support prior to the competition, as well as Michael Tautschnig for his help with judging. The organizers also thank the competition’s sponsors: Formal Methods Europe, Galois and Microsoft Research. Their financial support helped us to support participants with travel grants, and to finance the different prizes.