2023

verifyThis 2023 was organized by Xavier Denis and Stephen Siegel

Challenges

Challenge 1
DownloadList Reversal (PDF, 48 KB)

Challenge 2
DownloadBinary Decision Diagrams (PDF, 126 KB)

Challenge 3
DownloadNonblocking Concurrent Queue using LL/SC Synchronization (PDF, 95 KB)

Solutions

Click on the team to get to their solutions:

DownloadMartin Clochard and Yannick Moy (ZIP, 15 KB)

DownloadThibault Dardinier and Jonas Fiala (ZIP, 6 KB)

DownloadStephen 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