[fg-arc] VerifyThis 2023: Call for Problems

[Stephen Siegel]

          *** VerifyThis 2023: Call For Problems ***

CFP Deadline: February 1st, 2023
Website: http://verifythis.ethz.ch

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.

We are 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 on the VerifyThis web site, at the URL above.

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 at lri.fr and
siegel at 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.

Sincerely,

Stephen Siegel, University of Delaware <siegel at udel.edu>
Xavier Denis, Université Paris-Saclay <xldenis at lri.fr>
Co-chairs, VerifyThis 2023