<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p> </p>
<div class="moz-text-html" lang="x-unicode">
<h1 style="margin-bottom:6.0pt"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA"></span></h1>
<h1 style="margin-bottom:6.0pt"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA">*******************************************************************************</span></h1>
<h1 style="margin-bottom:6.0pt"><span class="spelle"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA">VerifyThis</span></span><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA"> Verification Competition 2024</span><span
lang="EN-CA"></span></h1>
<h1 style="margin-bottom:6.0pt"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA">ANNOUNCEMENT AND CALL FOR PROBLEMS</span><span
lang="EN-CA"></span></h1>
<h1 style="margin-bottom:6.0pt"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA">Competition to be held at ETAPS 2024</span><span
lang="EN-CA"></span></h1>
<h1 style="margin-bottom:6.0pt"><span lang="EN-CA"><a
href="http://verifythis.ethz.ch" target="_BLANK"><span
style="font-family:"Arial",sans-serif;color:#1155CC;font-weight:normal">http://verifythis.ethz.ch</span></a></span><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA"> </span><span lang="EN-CA"></span></h1>
<h1 style="margin-bottom:6.0pt"><span
style="font-size:11.0pt;font-family:"Arial",sans-serif;color:black;font-weight:normal"
lang="EN-CA">********************************************************************************</span><span
lang="EN-CA"></span></h1>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">Get involved, even if you cannot participate in
the competition: provide a challenge!</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">IMPORTANT DATES</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">Problems submission deadline: 15 December 2023</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">Competition: 6 and 7 April 2024</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">ABOUT THE COMPETITION</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span class="spelle"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">VerifyThis</span></span><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA"> 2024 will take place as part of the European
Joint Conferences on Theory and Practice of Software (ETAPS
2024) on 6 and 7 April 2019.</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">It is the 12th event in the <span class="spelle">VerifyThis</span>
competition series.</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">Information on previous events and participants
can be found at </span><span lang="EN-CA"><a
href="http://verifythis.ethz.ch" target="_BLANK"><span
style="font-family:"Arial",sans-serif;color:#1155CC">http://verifythis.ethz.ch</span></a></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">The aims of the competition are:</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">- to bring together those interested in formal
verification, and to provide an engaging, hands-on, and fun
opportunity for discussion.</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">- to evaluate the usability of program
verification techniques and tools.</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">The competition will offer a number of challenges
presented in natural language. Participants have to formalize
the requirements, implement a solution, and formally verify
the implementation for adherence to the specification.</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">There are no restrictions on the programming
language and verification technology used. Solutions will be
judged for correctness, completeness and elegance.</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">CALL FOR PROBLEMS</span><span lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">To be able to offer a broad and diverse set of
verification challenges, we are collecting submissions of
ideas for verification challenges and problems. We welcome
both problems of academic interest as well as challenges based
on themes that are relevant in industry.</span><span
lang="EN-CA"></span></p>
<p style="margin-bottom:12.0pt"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">The competition proceeds in three rounds. In each
round, participants are given 60 - 120 minutes to implement
and prove specified properties of a given algorithm and/or
data structure. They are free to use any verification tools
they choose. Challenges are typically concerned with proving
functional properties of the code in question (at least some
part of a challenge involves expressing and proving properties
specific to the algorithm/data structure in question). It is
common for problems to have multiple parts, e.g. to prove some
basic properties first, perhaps for a simplified case, and to
progress to more-advanced goals.<br>
<br>
We are looking for problem submissions. If you have recently
encountered an interesting challenge in your work where formal
techniques could be applied, please 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.<br>
<br>
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.
However, note that problem authors *are* allowed to
participate in the competition!<br>
<br>
Submissions should be sent by email to <a
href="mailto:alex.summers@ubc.ca"
class="moz-txt-link-freetext">alex.summers@ubc.ca</a> and <a
href="mailto:paula.herber@uni-muenster.de"
class="moz-txt-link-freetext">paula.herber@uni-muenster.de</a>.
The submission deadline is <b>December 15, 2023</b>. We look
forward to receiving your ideas!<b><br>
<br>
</b>Submission Criteria:</span><span lang="EN-CA"></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoNormal"
style="color:black;margin-top:12.0pt;mso-list:l0 level1
lfo1;vertical-align:baseline"> <span
style="font-family:"Arial",sans-serif"
lang="EN-CA">A brief yet precise problem description,
specifically identifying verification sub-tasks.</span><span
lang="EN-CA"></span></li>
<li class="MsoNormal" style="color:black;mso-list:l0 level1
lfo1;vertical-align:baseline"> <span
style="font-family:"Arial",sans-serif"
lang="EN-CA">A solution to the challenge is strongly
encouraged, otherwise please provide a sketch of
correctness.</span><span lang="EN-CA"></span></li>
<li class="MsoNormal"
style="color:black;margin-bottom:12.0pt;mso-list:l0 level1
lfo1;vertical-align:baseline"> <span
style="font-family:"Arial",sans-serif"
lang="EN-CA">The description document can use any reasonable
format, including plain text or PDF.</span><span
lang="EN-CA"></span></li>
</ul>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">ORGANIZERS</span><span lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Paula Herber, University of Münster, Germany</span><span
lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Alexander J. Summers, University of British
Columbia, Canada</span><span lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA"><br>
</span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">STEERING COMMITTEE</span><span lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Marieke Huisman, University of Twente, the
Netherlands</span><span lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Rosemary Monahan, Maynooth University Maynooth,
Ireland</span><span lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Peter Müller, ETH Zurich, Switzerland</span><span
lang="EN-CA"></span></p>
<p style="margin:0cm"><span
style="font-family:"Arial",sans-serif;color:black"
lang="EN-CA">* Mattias <span class="spelle">Ulbrich</span>,
Karlsruhe Institute of Technology, Germany</span></p>
<p></p>
<pre class="moz-signature" cols="72">--
Prof. Dr. Paula Herber
Embedded Systems Group
University of Münster
Computer Science Department, FB 10
Einsteinstr. 62, D-48149 Münster, Germany
Tel: +49 251 8332421
<a class="moz-txt-link-abbreviated moz-txt-link-freetext" href="mailto:paula.herber@uni-muenster.de">paula.herber@uni-muenster.de</a></pre>
</div>
<pre class="moz-signature" cols="72">--
Prof. Dr. Paula Herber
Embedded Systems Group
University of Münster
Computer Science Department, FB 10
Einsteinstr. 62, D-48149 Münster, Germany
Tel: +49 251 8332421
<a class="moz-txt-link-abbreviated" href="mailto:paula.herber@uni-muenster.de">paula.herber@uni-muenster.de</a></pre>
</body>
</html>