VerifyThis 2023

verifyThis 2023 was organized by Xavier Denis and Stephen Siegel.

Challenges

• Challenge 1: List Reversal (PDF, 48 KB)
• Challenge 2: Binary Decision Diagrams (PDF, 126 KB)
• Challenge 3: Nonblocking Concurrent Queue using LL/SC Synchronization (PDF, 95 KB)

Solutions

Click on the team to get to their solutions:

• Martin Clochard and Yannick Moy (ZIP, 15 KB)
• Thibault Dardinier and Jonas Fiala (ZIP, 6 KB)
• Stephen Siegel (ZIP, 34 KB)

Prizes

The winners from 2023 are:

• Best Team: “Somehow Alex & Marco Returned”: Alexander J. Summers and Marco Eilers\
• Best Student Team “Loops and Dots”: Jonas Fiala and Thibault Dardinier\
• Innovative Tool Feature: First class predicates in Gobra
  Used by team: “Wake Me Up When Verification Ends”, Linard Arquint and Joao Pereira
• Best Contributed Problem: Jean-​Christophe Filliatre and Andrei Paskevich, for List Reversal