At the KeY Symposium 2019 (Manigod, France), the VerifyThis Challenge has been announced. The challenge is currently rudimentary and will be updated soon. A mailing list is available for participants: verifythis-ltc@lists.kit.edu. For question, you can directly get in touch with organisers via the Github issues or email (verifythis-ltc-request@lists.kit.edu). Good luck. Marieke Huisman, Raul Monti, Mattias Ulbrich, Alexander Weigl
In the meantime, two different implementations of the key-server were created. Gidon Ernst created a Scala version: https://github.com/gernst/verifythis2020 I created a full java version (incl. a REST interface) https://github.com/wadoon/keyserver-java/ Author: Alexander Weigl, weigl@kit.edu
I have tried to formalise the natural language requirements into an Event-B model. It is not necessarily complete, and may not be fully in line with the natural language description. But it is a starting point for a discussion.
MCRL2 PGP protocol model A formalisation for the PGP protocol has been written as an MCRL2 model by Wytse Oortwijn from the VerCors team. You can find it here.
Dear fellows, the notification for the presentation are on the way to you. In the meantime, the ETAPS is postponed due to the COVID-19 spread. Our information are currently limited to the official information on the ETAPS front-page: https://www.etaps.org/. But we stick to the plan of having an on-site event with the VerifyThis workshop. Please stayed tuned in. When more information is available, we let you know on this web page and via the mailing-list verifythis-ltc@lists.
Dear fellows, We start with the preparation of an online event in which the submitted solution are presented and can be discussed. The online event is not an replacement of the onsite meeting. The onsite event will take place if/when the ETAPS and the VerifyThis workshop take place. Regards, Alexander
Dear all, the collection of extended abstracts for the contributions to the VerifyThis Long Term Challenge have been published as a technical report at KIT. You can find the proceedings here!
Dear all, A Dagstuhl meeting on Principles of Contract Languages had been because of the Covid-19 pandemic. Last April a number of groups participated in the online event for the Verify This Long Term Challenge 2020. As a follow-up on this, we would like to seize the opportunity to use the challenge and the available solutions to stipulate a discussion on the features that an ideal specification language would possess for this purpose.