Next Meeting: 23 January 2024
Posted on January 10, 2024
| ernst
The next discussion meeting will be on
23 January 2024, 10.00 CET.
Program
- Presentation by Aurel Bílý on their approach using Prusti
- Technical Discussions
- Collaboration and Follow-up
Registration:
Please sign up on the mailing list,
we will post the Zoom link shortly before the meeting; alternatively send an E-Mail directly to the organizers.
More Information
Memcached Challenge
Posted on April 21, 2023
| weigl
The second challenge will be disclosed at the ETAPS on Wed, 26th April 2023.
The introduction is scheduled in the TOOLympics session.
Next Meeting: 24 March 2022
Posted on February 26, 2022
| weigl
Dear fellows,
the next discussion meeting will be on
24 March 2022, 14.00 CEST.
More Information
Regards,
Alexander
Next Meeting: 29 September 2021
Posted on August 13, 2021
| weigl
Dear fellows,
the next discussion meeting will be on
29 September 2021, 14.00 CEST.
More Information
Regards,
Alexander
Online Discussion
Posted on November 20, 2020
| ulbrich
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.
[Read More]Proceedings for the contributions available
Posted on June 26, 2020
| ulbrich
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!
Online Event
Posted on April 7, 2020
| weigl
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
Posted on March 17, 2020
| weigl
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.
[Read More]MCRL2 PGP model
Posted on September 23, 2019
| monti
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
Posted on September 10, 2019
| ulbrich
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.
Formalisation of the key manager This Event-B model is an attempt to formalise the requirements of the VerifyThis Long Term Challenge 2020. It is deliberately kept on a very high level of abstraction, but should have enough detail to clarify the behaviour of the system.
[Read More]