VerifyThis 2025

VerifyThis 2025 was organized by Thomas Wies (New York University) and Jenna DiVincenzo (Purdue University) and took place at ETAPS 2025 at the McMaster University, Hamilton, Canada.

Challenges

• Challenge 1: Minimum Excludant (PDF), suggested by J.C. Filliâtre
• Challenge 2: Linus Torvald’s Elegant Linked-List Removal (PDF), suggested by Ștefan Ciobâcă
• Challenge 3: Persistent Arrays (PDF)
• Challenge 4: Persistent Disjoint Sets (PDF)

Solutions

• … more to follow.

Prizes — The winners 2025 are:

• Overall Best Team: “Ghost in the Loop”: Jonáš Fiala and Thibault Dardinier (Student Team)
• Best 1-person Team: “Lurking in the Grass”: Alexander Summers
• Most Impressive Tool Medley: “The Marians”: Marian Lingsch-Rosenfeld and Gidon Ernst
• Best Contributed Problem: Ștefan Ciobâcă
• Innovative Tool Feature: Model checking based on symbolic execution used by the “Delaware Blue Hens”: Stephen Siegel and Alex Wilton
• Innovative Tool Feature: Fully automated memory safety verification with Broom used by “IsaTUW”: Florian Sextl

Employed tools and number of teams:

• Dafny (4)
• Viper (3)
• Isabelle (2)
• Broom (1)
• Civl [model checker by Siegel et al.] (1)
• Liquid Haskell (1)
• SecC (1)
• VerCors (1)
• Verus (1)
• Why3 (1)

Sponsors

We gratefully acknowledge generous sponsorship from Amazon Web Services

and Certora