Online Discussion Feb 15, 2023, 08:00 UTC - 09:30 UHR UTC Feb 15, 2023, 09:00 CET - 10:30 UHR CET Feb 15, 2023, 19:00 AEDT - 20:30 UHR EDT Information for participating are below. Backgrund: The VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort. We initially looked HAGRID as a case study, but have since moved on to considering a simple Solidity casino as the running example. [Read More]

July 13, 2022, 12:00 UTC - 14:00 UHR UTC July 13, 2022, 14:00 CEST -16:00 UHR CEST July 13, 2022, 08:00 EDT - 10:00 UHR EDT Information for participating are below. Backgrund: The VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort. We initially looked HAGRID as a case study, but have since moved on to considering a simple Solidity casino as the running example. [Read More]

March 24, 2022, 12:00 UTC - 14:00 UHR UTC March 24, 2022, 14:00 CEST -16:00 UHR CEST March 24, 2022, 08:00 EDT - 10:00 UHR EDT Information for participating are below. Backgrund: The VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort. We initially looked HAGRID as a case study, but have since moved on to considering a simple Solidity casino as the running example. [Read More]

December 15, 2021, 12:00 UTC - 14:00 UHR UTC December 15, 2021, 14:00 CST -16:00 UHR CST December 15, 2021, 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]

September 29, 2021, 12:00 UTC - 14:00 UHR UTC September 29, 2021, 14:00 CEST -16:00 UHR CEST September 29, 2021, 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]

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]