Casino-Example #4


Online Discussion

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 have two talks:

  • Jonas Schiffl on TLA translations for Smart Contracts,
  • Mattias Ulbrich on his concept of Co-Contracts.

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.


See also