Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] VerifyThis 2022 --- Call for Problems

view this post on Zulip Email Gateway (Oct 12 2021 at 17:25):

From: Peter Lammich <>
VerifyThis 2022: Call for Problems

apologies for multiple postings.
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—2021.

To extend the problem pool and tend better to the needs of the
participants, we are soliciting verification problems for the

A problem should contain an informal statement of the algorithm to be
implemented (optionally with complete or partial pseudo code) and the
requirement(s) to be verified.
A problem should be suitable for a 60—90 minute time slot.
Submission of reference solutions is strongly encouraged.
Problems with an inherent language- or tool-specific bias should be
clearly identified as such.
Problems that contain several subproblems or other means of difficulty
scaling are especially welcome.
The organizers reserve the right (but no obligation) to use the
problems in the competition, either as submitted or with modifications.
Submissions from (potential) competition participants are allowed.

Problems from previous competitions can be seen at the archive.

Please send submissions via email to by
January 31, 2022.

The most suitable submission for competition will receive a prize.

Last updated: Jan 24 2022 at 23:18 UTC