VerifyThis Competition
2025 edition at ETAPS 2025 in Hamilton, Canada - consider the Participation link below!
About
VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015–2024. The challenge problems and solutions of previous competitions are available in the archive.
The aims of the competition are:
- 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 program verification techniques and tools.
The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
The use of AI-based tools is allowed; solutions to challenges need to mention which AI tools were used, if any.
2025 Organizers
- Jenna DiVincenzo, Purdue, jennad@purdue.edu
- Thomas Wies, NYU, wies@cs.nyu.edu
More information
Steering Committee
- Marieke Huisman, University of Twente, the Netherlands
- Rosemary Monahan, Maynooth University Maynooth, Ireland
- Peter Müller, ETH Zurich, Switzerland
- Mattias Ulbrich, Karlsruhe Institute of Technology, Germany
Sponsors
If you want to sponsor the VerifyThis 2025 event, feel free to contact us.
Related Events and Activities
More-recently, there have also been VerifyThis Long-Term Challenges designed for informal comparison and collaborations over several months: see https://verifythis.github.io/ for details.
Related events also include the Verified Software Competition (VSComp: http://sites.google.com/a/vscomp.org/main/, https://sites.google.com/site/vstte2012/compet, http://www.vscomp.org) held online and the Competition on Software Verification](http://sv-comp.sosy-lab.org/) focusing on evaluating systems in a way that does not require user interaction. SV-COMP is associated with TACAS.
VerifyThis is also a collection of verification problems (and solutions). Its counterpart is VerifyThus—a distribution of deductive verification tools for Java-like languages, bundled and ready to run in a VM. Both were created with support from COST Action IC0701.
A workshop on comparative empirical evaluation of reasoning systems COMPARE2012 was held on June 30th at IJCAR 2012 in Manchester. Competitions were one of the main topics of the workshop.