- 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.
Agenda: We will continue and deepen this discussion by trying to identify how different approaches can exchange informations. We will compare artifacts and specififications and will see what each approach could provide and where it could benefit from other tools.
To this end, we have collected the solutions presented last time as in a fact sheet gallery quickly summarising the approaches and provided models/implementations.
It will be the goal of the time until the meeting and of the meeting itself to fill the items in “Can offer” and “Look for”.
We present some ideas on how contracts can be used to communicate between different verification approaches.
Aggregated Materials
Who can join the meeting?
Everybody who is interested in the challenge, formal verification, the proposed solutions or VerifyThis is cordially invited to join the meeting!
How can I join the meeting?
The online event takes place with Zoom.
In protection against spammers, we require a short registration beforehand. The login credentials will be sent via your provided email address. Please register yourself with an email to weigl@kit.edu.
Note: If you had already registered for a previous online event, we will send you the required login credentials automatically. Another registration is not required in this case.