hagrid

Online Discussion June 23, 12:00 UTC 14:00 UHR UTC June 23, 14:00 CEST -16:00 UHR CEST June 23, 08:00 EDT 10:00 UHR EDT 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. [Read More]

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. [Read More]

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. [Read More]

Online Discussion 12th February, 2020, 14:00 – 16:00 UTC 14:00 UTC 16: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 2020 four approaches to the verification challenge have been submitted to and presented during an online workshop, and in November 2020, a follow-up online discussion revealed interesting new ideas regarding specification and verifiation of interacting systems like Hagrid. [Read More]