2015

The competition report can be found Downloadhere (PDF, 452 KB)vertical_align_bottom

Winners

• 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: (2x)
  • * Why3 for the lemma library (as demonstrated by its use in the competition)
  • * 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

Challenges

Competition challenges will be posted here. Tentative schedule for April 12th:

• DownloadProblem 1 (PDF, 40 KB)vertical_align_bottom announced at 9:00 (60 minutes) - this problem was submitted by external pageThomas Genetcall_made
  
• DownloadProblem 2 (PDF, 39 KB)vertical_align_bottom announced at 10:15 (60 minutes)
• DownloadProblem 3 (PDF, 37 KB)vertical_align_bottom announced at 11:30 (90 minutes)

Solutions

The Downloadsolutions (ZIP, 5 KB)vertical_align_bottom developed by participants during the competition, and polished afterwards. Solutions may be updated as time goes on.

• external pageJean-Christophe Filliâtre & Guillaume Melquiond (Why3)call_made
• external pageGidon Ernst & Jörg Pfähler (KIV)call_made
• Nadia Polikarpova & Carlo A. Furia (AutoProof): external pagerelaxed prefixcall_made, external pagegcdcall_made, external pagedancing listscall_made
• external pageRustan Leino (Dafny)call_made
• Jan Friso Groote (mCRL2), attached to this page: external pagerelaxed prefixcall_made, external pagegcdcall_made, external pagedancing listscall_made

RULES

1. Solutions are to be submitted per email
   
2.  Submissions must state the version of the verification system used (for development versions, internal revision, timestamp, or similar unique id).
3. The main rule of the competition is no cheating is allowed. The judges may penalize or disqualify entrants in case of unfair competition behavior and may adjust the competition rules to prevent future abuse.
4. It is allowed to modify the verification system during the competition. This is to be noted in the solution(s)
5. All techniques used must be general-purpose, and are expected to extend usefully to new unseen problems
6. Internet access is allowed, but using the interget to search for problem solutions is not.
7. Involvement of other people beyond those on the team is not allowed.
8. While care is taken to ensure correctness of the reference implementations supplied with problem descriptions, the organizers do not guarantee that they are indeed correct.

(We acknowledge Geoff Sutcliffe for inspiring/suggesting some of these rules.)