VerifyThis Casino Challenge Artifact Repository

Fuente: Zenodo
Salvato in:
Dettagli Bibliografici
Autori principali: Weigl, Alexander, Merz, Stephan, Schiffl, Jonas, Becker-Kupczok, Jonas, Eilers, Marco, Ahrendt, Wolfgang, Monti, Raul E., Bliudze, Simon
Natura: Recurso digital
Pubblicazione: Zenodo 2025
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866901697856536576
author Weigl, Alexander
Merz, Stephan
Schiffl, Jonas
Becker-Kupczok, Jonas
Eilers, Marco
Ahrendt, Wolfgang
Monti, Raul E.
Bliudze, Simon
author_facet Weigl, Alexander
Merz, Stephan
Schiffl, Jonas
Becker-Kupczok, Jonas
Eilers, Marco
Ahrendt, Wolfgang
Monti, Raul E.
Bliudze, Simon
contents <p>This repository contains the material of the [Casino case study](https://verifythis.github.io/02casino/). In this paper we discuss several specification solutions. In particular you find the following solutions:</p> <p>* [uppaal]      -- Timed automata<br>* [supervisory] -- Nonblocking verification<br>* [tlaplus]  -- State machine specification with model checking<br>* [solc-verify]  -- Source-level deductive verification<br>* [secc]     -- Deductive verification<br>* [vercors]  -- Deductive verification<br>* [javabip]  -- Deductive verification of component-based systems<br>* [2vyper] -- Deductive verification with resource-based specifications</p>
format Recurso digital
id zenodo_https___doi_org_10_5281_zenodo_16318664
institution Zenodo
language
publishDate 2025
publisher Zenodo
record_format zenodo
spellingShingle VerifyThis Casino Challenge Artifact Repository
Weigl, Alexander
Merz, Stephan
Schiffl, Jonas
Becker-Kupczok, Jonas
Eilers, Marco
Ahrendt, Wolfgang
Monti, Raul E.
Bliudze, Simon
<p>This repository contains the material of the [Casino case study](https://verifythis.github.io/02casino/). In this paper we discuss several specification solutions. In particular you find the following solutions:</p> <p>* [uppaal]      -- Timed automata<br>* [supervisory] -- Nonblocking verification<br>* [tlaplus]  -- State machine specification with model checking<br>* [solc-verify]  -- Source-level deductive verification<br>* [secc]     -- Deductive verification<br>* [vercors]  -- Deductive verification<br>* [javabip]  -- Deductive verification of component-based systems<br>* [2vyper] -- Deductive verification with resource-based specifications</p>
title VerifyThis Casino Challenge Artifact Repository
url https://doi.org/10.5281/zenodo.16318664