Online Result and Exchange Event
27th April 2020, 10:00 UTC
A final workshop session for the challenge had been planned at ETAPS (along with the VerifyThis program verification competition). Since ETAPS has been postponed, we will meet and exchange online. We have received several 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.
- (10:00 UTC)
- Greeting and Introduction to the VerifyThis Longterm Challenge 2020 by the organizers
- (10:20 UTC)
Gidon Ernst and Lukas Rieger
Information Flow Testing of a PGP Keyserver
- (10:50 UTC)
Diego Diverio, Cláudio Lourenço and Claude Marché
"You-Know-Why": an Early-Stage Prototype of a Key Server Developed using Why3
- (11:20 UTC)
- Break (10 minutes).
- (11:30) UTC)
Stijn de Gouw, Mattias Ulbrich and Alexander Weigl
The KeY Approach on Hagrid
- (12:00 UTC)
Claire Dross, Johannes Kanig, and Yannick Moy
A Solution to the Long-Term Challenge in SPARK
- (12:30 UTC)
Gidon Ernst, Toby Murray and Mukesh Tiwari
Verifying the Security of a PGP Keyserver
- (13:00 UTC)
- Final discussion and feedback to the challenge.
- (13:30 UTC)
Who can join the meeting?
Everybody who is interested about the challenge, formal verification, the proposed solutions and VerifyThis is cordially to join the meeting!
How can I join the meeting?
The online event takes place with BlueJeans.
In protection against spammers, we require a short registration beforehand. The login credentials will
be sent via your provided email address. Please register yourself via our
or with a email to
weigl at kit dot edu.
Update (2020-04-24, 13:00 o'clock): We have sent out the meeting information. If you registered before this time, you should have got an email.
Registration is still open. The meeting information will be sent manually and might take some hours.
If you havn't got any meeting information (meeting URL + id) until Sunday
evening. Please just write me (
weigl at kit dot edu) short
message. I have might miss you.
Please respect the following simple meeting rules to have a productive meeting:
- use your real-name (you can change it under "Poeple/Participants" in BlueJeans after joining the room.)
- dial in 5 minutes in advance
- mute when not speaking (avoid noise)
- join with disabled microphone and video
- use a headset if possible (avoid reverberation)