<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">********************************************************************************<br>
<br>
VerifyThis Verification Competition 2021<br>
<br>
CALL FOR PARTICIPATION -- GRANTS -- PRIZES<br>
<br>
Competition to be held at ETAPS 2021 (Virtual)<br>
<br>
<a href="http://verifythis.ethz.ch" target="_blank">http://verifythis.ethz.ch</a>
<br>
<br>
********************************************************************************<br>
<br>
IMPORTANT DATES<br>
<br>
Registration deadline: March 13, 2021<br>
Competition: March 26 and 27, 2021<br>
<br>
ABOUT THE COMPETITION<br>
<br>
VerifyThis 2021 is a program verification competition taking place as part of<br>
the European Joint Conferences on Theory and Practice of Software (ETAPS 2021)<br>
on 26 and 27 March 2021. It is the 9th event in the VerifyThis competition<br>
series. Information on previous events and participants can be found at:<br>
<a href="http://verifythis.ethz.ch" target="_blank">http://verifythis.ethz.ch</a><br>
<br>
The aims of the competition are:<br>
- to bring together those interested in formal verification, and to provide<br>
an engaging, hands-on, and fun opportunity for discussion, and<br>
- to evaluate the usability of logic-based program verification tools in a<br>
controlled experiment that could be easily repeated by others.<br>
<br>
The competition will offer a number of challenges presented in natural language<br>
and pseudo code. Participants have to formalize the requirements, implement a<br>
solution, and formally verify the implementation for adherence to the<br>
specification.<br>
<br>
There are no restrictions on the programming language and verification<br>
technology used. The correctness properties posed in problems will have the<br>
input-output behaviour of programs in focus. Solutions will be judged for<br>
correctness, completeness and elegance.<br>
<br>
PARTICIPATION<br>
<br>
Participation is open for anybody interested. Teams of up to two people are<br>
allowed. VerifyThis will be a virtual event with some synchronous sessions via<br>
video call, and a 24 hour window for teams to solve problems at their own<br>
convenience. More details and a full program will be announced on the website.<br>
<br>
We particularly encourage participation of:<br>
- people from under-represented communities<br>
- student teams (this includes PhD students)<br>
- non-developer teams using a tool someone else developed<br>
- several teams using the same tool<br>
<br>
GRANTS<br>
<br>
The competition has funds for a limited number of registration grants, sponsored<br>
by Amazon AWS. Grants will cover the registration costs for ETAPS. To apply for<br>
a grant, fill out the relevant section of the registration form and, if you are<br>
a student, have your supervisor send a brief letter of support to the following<br>
address:<br>
<a href="mailto:verifythis@googlegroups.com" target="_blank">verifythis@googlegroups.com</a><br>
<br>
PRIZES<br>
<br>
Thanks to our sponsors, VerifyThis typically offer team prizes such as the best<br>
overall team, the most distinguished tool features and the best student team.<br>
As VerifyThis 2021 will be a virtual event, we plan to increase the number of<br>
team prizes and the prize money amount this year. VerifyThis 2021 prizes are<br>
sponsored by Amazon AWS.<br>
<br>
REGISTRATION<br>
<br>
Please register by filling out the following form:<br>
<a href="https://forms.gle/kZpGKMVkRrRyidiq8" target="_blank">https://forms.gle/kZpGKMVkRrRyidiq8</a><br>
<br>
Deadline: March 13, 2021<br>
<br>
ORGANIZERS<br>
* Siddharth Krishna, Microsoft Research Cambridge, UK<br>
* Wytse Oortwijn, ESI (TNO), Netherlands<br>
<br>
STEERING COMMITTEE<br>
* Marieke Huisman, University of Twente, the Netherlands<br>
* Rosemary Monahan, Maynooth University, Ireland<br>
* Peter Müller, ETH Zurich, Switzerland<br>
* Mattias Ulbrich, Karlsruhe Institute of Technology, Germany<br>
<br>
CONTACT<br>
Email: <a href="mailto:verifythis@googlegroups.com" target="_blank">verifythis@googlegroups.com</a><br>
Web: <a href="http://verifythis.ethz.ch" target="_blank">http://verifythis.ethz.ch</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>