[TYPES/announce] VerifyThis 2025 - Call for Participation

[Thomas Wies]

[Apologies in case of multiple posting]

********************************************************************************

VerifyThis Verification Competition 2025
CALL FOR PARTICIPATION
Competition to be held at ETAPS 2025
https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4exsD_vb3Q$ 
********************************************************************************

IMPORTANT DATES

Travel grant application deadline: TBA on the VerifyThis website 
(https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4exsD_vb3Q$ ) at a later date.

Early registration deadline (physical attendees): February 28, 2025
Normal registration deadline (physical attendees): March 21, 2025
Registration deadline (virtual attendees): April 18, 2025

Competition: May 3rd and 4th, 2025

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 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.

PARTICIPATION

Participation is open for anybody interested. Teams of up to two people 
are allowed. VerifyThis will be held as a hybrid workshop as part of 
ETAPS 2025 in Hamilton, Canada. Registration for physical attendance of 
ETAPS workshops is required. Early registration is open until February 
28. To register as a physical attendee, please go to 
https://urldefense.com/v3/__https://etaps.org/2025/registration/__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4eypgyIrjg$  and register for both Saturday and 
Sunday. The actual competition will happen on the first day, whereas the 
second day will be used to discuss and evaluate the solutions.

To register as a virtual attendee, please complete the registration form 
at https://urldefense.com/v3/__https://forms.gle/BRh56QLu34aor8QA7__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4eyas1jXRA$ .

More details and a full program will be announced on the VerifyThis 
website https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4exsD_vb3Q$ .

We particularly encourage participation of:
   * student teams (this includes PhD students)
   * non-developer teams / using a tool someone else developed
   * several teams using the same tool

TRAVEL GRANTS
We anticipate having funds for a limited number of travel grants to 
cover the incurred travel and accommodation costs up to a certain limit. 
More details about the travel grants, application deadline, and 
application process will be announced at a later date on the VerifyThis 
website https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!RSKxwBcTXf2prT7kZBcv8eoAsO7s6YFtbSv1tyCHnoHgQBZZL8laLAZhb3ARcuAG3xo9R_jBF05B-00us7gV4exsD_vb3Q$ .

ORGANIZERS
* Jenna DiVincenzo, Purdue University, USA
* Thomas Wies, New York University, USA

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