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]
general 

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

general  corona 

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]
general  corona 

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.

general  formal model  MCRL2 

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]
general