<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style>
<!--
@font-face
{font-family:Wingdings}
@font-face
{font-family:"Cambria Math"}
@font-face
{font-family:Calibri}
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif}
h1
{margin-right:0cm;
margin-left:0cm;
font-size:24.0pt;
font-family:"Calibri",sans-serif;
font-weight:bold}
a:link, span.MsoHyperlink
{color:#0563C1;
text-decoration:underline}
a:visited, span.MsoHyperlinkFollowed
{color:#954F72;
text-decoration:underline}
span.EmailStyle17
{font-family:"Calibri",sans-serif;
color:windowtext}
span.Heading1Char
{font-family:"Calibri",sans-serif;
font-weight:bold}
span.SpellE
{}
.MsoChpDefault
{font-family:"Calibri",sans-serif}
@page WordSection1
{margin:72.0pt 72.0pt 72.0pt 72.0pt}
div.WordSection1
{}
ol
{margin-bottom:0cm}
ul
{margin-bottom:0cm}
-->
</style>
</head>
<body lang="EN-CA" link="#0563C1" vlink="#954F72" style="">
<div class="WordSection1">
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">*******************************************************************************</span></h1>
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><span class="SpellE"><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">VerifyThis</span></span><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">
Verification Competition 2024</span></h1>
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">ANNOUNCEMENT AND CALL FOR PROBLEMS</span></h1>
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">Competition to be held at ETAPS 2024</span></h1>
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><a href="https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!V791D22bNZMVJoYIX_AUKS8r1HtfgxLh36uwnfsjF9wBpJAT_QDXzWc1XkdUm_83FN1t569K1pk45BnPs1OrZu5Uzt1hW1SUR--r$" target="_BLANK"><span style="font-family:"Arial",sans-serif; color:#1155CC; font-weight:normal">http://verifythis.ethz.ch</span></a><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal"> </span></h1>
<h1 style="margin-right:0cm; margin-bottom:6.0pt; margin-left:0cm"><span style="font-size:11.0pt; font-family:"Arial",sans-serif; color:black; font-weight:normal">********************************************************************************</span></h1>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">Get involved, even if you cannot participate in the competition: provide a challenge!</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">IMPORTANT DATES</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">Problems submission deadline: 15 December 2023</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">Competition: 6 and 7 April 2024</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">ABOUT THE COMPETITION</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span class="SpellE"><span style="font-family:"Arial",sans-serif; color:black">VerifyThis</span></span><span style="font-family:"Arial",sans-serif; color:black"> 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></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">It is the 12th event in the
<span class="SpellE">VerifyThis</span> competition series.</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">Information on previous events and participants can be found at
</span><a href="https://urldefense.com/v3/__http://verifythis.ethz.ch__;!!IBzWLUs!V791D22bNZMVJoYIX_AUKS8r1HtfgxLh36uwnfsjF9wBpJAT_QDXzWc1XkdUm_83FN1t569K1pk45BnPs1OrZu5Uzt1hW1SUR--r$" target="_BLANK"><span style="font-family:"Arial",sans-serif; color:#1155CC">http://verifythis.ethz.ch</span></a></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">The aims of the competition are:</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">- to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion.</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">- to evaluate the usability of program verification techniques and tools.</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">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></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">There are no restrictions on the programming language and verification technology used. Solutions will be judged for correctness, completeness
and elegance.</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">CALL FOR PROBLEMS</span></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">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></p>
<p style="margin-right:0cm; margin-bottom:12.0pt; margin-left:0cm"><span style="font-family:"Arial",sans-serif; color:black">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 alex.summers@ubc.ca and paula.herber@uni-muenster.de. The submission deadline is
<b>December 15, 2023</b>. We look forward to receiving your ideas!<b><br>
<br>
</b>Submission Criteria:</span></p>
<ul type="disc" style="margin-top:0cm">
<li style="color:black; margin-top:12.0pt; margin-bottom:0cm; margin-bottom:.0001pt; vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">A brief yet precise problem description, specifically identifying verification sub-tasks.</span></li><li style="color:black; margin-top:0cm; margin-bottom:0cm; margin-bottom:.0001pt; vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">A solution to the challenge is strongly encouraged, otherwise please provide a sketch of correctness.</span></li><li style="color:black; margin-top:0cm; margin-bottom:12.0pt; vertical-align:baseline">
<span style="font-family:"Arial",sans-serif">The description document can use any reasonable format, including plain text or PDF.</span></li></ul>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">ORGANIZERS</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Paula Herber, University of Münster, Germany</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Alexander J. Summers, University of British Columbia, Canada</span></p>
<p class="MsoNormal"> </p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">STEERING COMMITTEE</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Marieke Huisman, University of Twente, the Netherlands</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Rosemary Monahan, Maynooth University Maynooth, Ireland</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Peter Müller, ETH Zurich, Switzerland</span></p>
<p style="margin:0cm; margin-bottom:.0001pt"><span style="font-family:"Arial",sans-serif; color:black">* Mattias
<span class="SpellE">Ulbrich</span>, Karlsruhe Institute of Technology, Germany</span></p>
<p class="MsoNormal"> </p>
<p class="MsoNormal"> </p>
<p class="MsoNormal"><a name="_MailAutoSig"><span lang="EN-GB" style="">Best wishes,</span></a></p>
<p class="MsoNormal"><span style=""><span lang="EN-GB" style="">Alex</span></span></p>
<span style=""></span>
<p class="MsoNormal"> </p>
</div>
</body>
</html>