What is VerifyThis?

The VerifyThis verification competition is a regular event run as an onsite meeting with workshop character in which three challenges are proposed that participants have to verify in 90 minutes each using their favourite program verification tool.

We have experienced that the state of the art of program verification allows the participants to specify and verify impressively complex algorithms in this short a time span. If such sophisticated, realistic but not real, problems can be solved in real-time, what would be achievable if (a)~we as the program verification community collaborated and (b)~the time constraints were removed?

The Challenge

This VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort.

For this year, we selected HAGRID, a PGP-keyserver, for the challenge. HAGRID is a fresh development, which became necessary as the old keyserver (SKS) is vulnerable against DoS attacks CVE-2019-13050, is not conform with GPRD, and had performance issues. More background information are available in the blog post of the developers HAGRID is already in production.

How to participate?

Participation on the challenge is easy. You should pick your favourite tool for the formal software assessment, and try whether you find a bug or prove adhering of the specification in HAGRID (or a suitable abstraction). Of course you can participate in groups. Moreover, we would like to foster collaboration between participating groups. Therefor we would appreciate if you register your group. Do not forget to also subscribe to our mailing list (verifythis-ltc@lists.kit.edu) to be able to share your questions and your work and to keep up to date with the work of the rest of the teams.

We plan to publish on the VerifyThis workshop at the ETAPS2020, where we kindly invite each participant to present their results of this challenge.

News