The Coq mailing list

["r.e.monti AT utwente.nl" <r.e.monti AT utwente.nl>]

                    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/