[Jmlspecs-interest] VTLTC 2020 - Call for Online Participation

[<r.e...@ut...>]

                    Call for Online Participation.


                 VerifyThis Long-Term Challenge 2020

                -- Online Result and Exchange Event --

                   27th April 2020, 10:00 UTC [0]

           >>> https://verifythis.github.io/online-event <<<



## Introduction

The VerifyThis  Long-Term Challenge complements the  on-site format of
the  VerifyThis competition  with a  verification challenge,  in which
teams contribute to  the verification of a  practically relevant piece
of software over a  longer period of time. The challenge  aims to be a
showcase  that deductive  program  verification  can produce  relevant
results for real systems with acceptable effort.

The challenge system  to be verified is the new  implementation of the
PGP server  infrastructure, called HAGRID [2].  The old implementation
did not  conform to GDPR  and was known  to be vulnerable  against DoS
attacks.


## The Online Result and Exchange Workshop

A final workshop  session for the challenge had been  planned at ETAPS
(along  with the  VerifyThis  program  verification competition  [1]).
Since ETAPS has been postponed, we will meet and exchange online.

We have received  five submissions that each contribute  a solution to
different  aspects  of  the challenge  using  different  abstractions,
different assumptions and different verification techniques.

During this  online meeting, the  different solutions will  be briefly
explained, and  we discuss the  approaches, how they can  benefit from
one another and how further verification success can be stipulated.

This meeting is not meant as a replacement of the on-site event.  It
is meant as an informal event to exchange ideas, to give positive
impulses on further advances of approaches, or on how to combine
solutions. If the situation permits, the onsite event will take place
in autumn during ETAPS.


## Call for Participation

Everybody  who  is  interested   about  the  challenge,  the  proposed
solutions and VerifyThis is cordially invited to join the meeting!


## Online Link

More information on how to participate, agenda and resources are on
our webpage of the online workshop:

           >>> https://verifythis.github.io/online-event  <<<


## Program Chairs and Organizers

Marieke Huisman                 Raul E. Monti

Mattias Ulbrich                 Alexander Weigl


[0] Find out your local time here:
https://www.timeanddate.com/worldclock/fixedtime.html?msg=VerifyThis&iso=2020-04-27T10:00:00

[1] https://www.pm.inf.ethz.ch/research/verifythis.html

[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/