<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="Apple-Mail-URLShareUserContentTopClass"><br></div><div class="Apple-Mail-URLShareWrapperClass" style="position: relative !important;"><blockquote type="cite" style="border-left-style: none; color: inherit; padding: inherit; margin: inherit;">
*** VerifyThis 2023: Call For Problems ***<br><br>CFP Deadline: February 1st, 2023<br>Website: http://verifythis.ethz.ch<br><br>VerifyThis is an annual program verification competition held as part<br>of ETAPS. It is an opportunity for community members and tool authors<br>to showcase their work and learn from each other with hands-on<br>exercises.<br><br>The competition proceeds in three rounds. In each round, participants<br>are given 90 minutes to implement and prove specified properties of a<br>given algorithm and/or data structures. They are free to use any<br>verification tools they choose.<br><br>We are looking for problem submissions. If you have recently<br>encountered an interesting challenge in your work, don’t hesitate to<br>submit it. Typical challenges have clear input-output specifications<br>and often incorporate one or more of the following: heap allocation,<br>concurrency, arithmetic reasoning. A challenge usually describes a<br>problem using natural language together with some pseudocode, and then<br>provides a list of properties or “verification tasks” of varied levels<br>of difficulty. Contributors are encouraged to look at the Archive of<br>previous problems on the VerifyThis web site, at the URL above.<br><br>An award will be given for any submission used in the competition.<br><br>To avoid spoiling the competition for others, we ask that you keep the<br>subject of your submission private.<br><br>Submissions should be sent by email to xldenis@lri.fr and<br>siegel@udel.edu.<br><br>Submission Criteria:<br><br>* A brief yet precise problem description, specifically identifying<br>verification sub-tasks.<br><br>* A solution to the challenge is strongly encouraged, otherwise<br>please provide a sketch of correctness.<br><br>* The description document can use any reasonable format, including<br>plain text or PDF.<br><br>Sincerely,<br><br> Stephen Siegel, University of Delaware <siegel@udel.edu><br> Xavier Denis, Université Paris-Saclay <xldenis@lri.fr><br> Co-chairs, VerifyThis 2023
</blockquote></div></body></html>