Deadline: February 1st, 2023
VerifyThis is an annual program verification competition held as part of ETAPS. It is an opportunity for community members and tool authors to showcase their work and learn from each other with hands-on exercises.
The competition proceeds in three rounds. In each round, participants are given 90 minutes to implement and prove specified properties of a given algorithm and/or data structures. They are free to use any verification tools they choose.
Xavier Denis and I are co-chairing VerifyThis 2023. We are currently looking for problem submissions. If you have recently encountered an interesting challenge in your work, don’t hesitate to submit it. Typical challenges have clear input-output specifications and often incorporate one or more of the following: heap allocation, concurrency, arithmetic reasoning. A challenge usually describes a problem using natural language together with some pseudocode, and then provides a list of properties or “verification tasks” of varied levels of difficulty. Contributors are encouraged to look at the Archive of previous problems.
An award will be given for any submission used in the competition.
To avoid spoiling the competition for others, we ask that you keep the subject of your submission private.
Submissions should be sent by email to xldenis@lri.fr and siegel@udel.edu.
Submission Criteria:
- A brief yet precise problem description, specifically identifying verification sub-tasks.
- A solution to the challenge is strongly encouraged, otherwise please provide a sketch of correctness.
- The description document can use any reasonable format, including plain text or PDF.