Timeline
Contract Languages II: Reiner Hähnle: Context-aware Trace Contracts – 10 July 2024
Jul 3, 2024
Reiner Hähnle will present work on Context-aware Trace Contracts.
Time and Date: 10 July, 16.00 CEST, for Link see below.
Contract Languages I: Alessandro Cimatti: Software Contracts meet System Contracts – 15 May 2024
May 15, 2024
As a follow-up to the March 2024 Lorentz Center workshop on Contract
Languages, we
host a series of online presentations and discussions around
formal methods with contract languages, aligning with the LTC goal of
enabling information exchange between different formal systems.
Memcached Online Discussion
Jan 23, 2024
The next discussion meeting will be on January 23, 2024, 10:00 CET -12:00 CET.
Memcached Challenge
Apr 21, 2023
The Memcached challenge was disclosed at the ETAPS on Wed, 26th April 2023.
The introduction was scheduled in the TOOLympics session.
Casino Example #5: Finalisation of the Example
Feb 15, 2023
Last online discussion on the Casino example.
Casino-Example #4
Jul 13, 2022
Online-Discussion on the Casino Example.
Casino Example #3
Mar 24, 2022
The next discussion meeting will be on 24 March 2022, 14.00 CEST.
Casino Example #2
Dec 15, 2021
Online Discussion on the Casino Example.
Casino Example #1
Sep 29, 2021
Online Discussion on the Casino Example.
Specification Language #2
Jun 23, 2021
Online Discussion on Hagrid.
Specification Languages
Nov 27, 2020
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.
Online Discussion
Nov 20, 2020
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.
Proceedings for the contributions available
Jun 26, 2020
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!
Hagrid Results #2
Online Result and Exchange Event
Apr 27, 2020
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.
Online Event
Apr 7, 2020
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
ETAPS & COVID-19
Mar 17, 2020
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.
Hagrid Results #1
Feb 12, 2020
Online Discussion
12th February, 2020, 14:00 – 16:00 UTC 14:00
UTC
MCRL2 PGP model
Sep 23, 2019
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.
Event-B Formalisation
Sep 10, 2019
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.
Scala and Java Implementations
Sep 10, 2019
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
Challenge start
Aug 12, 2019
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
Jan 1, 1