Hagrid

Hagrid Results #2

27th April 2020, 10:00 UTC Information for participating are below. 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.

Specification Languages

27th November 2020, 10:00 UTC Information for participating are below. The VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort. We selected HAGRID, a recently developed PGP-keyserver, for the challenge. Its development became necessary as the old keyserver had serious data protection and security issues. In April four approaches to the verification challenge have been submitted to and presented during an online workshop.