Companion repository with the artifacts to the Casino case study
Working title: From Model Checking to Deductive Verification: A Smart Contract as a Challenge for State-of-the Art Formal Specification and Verification Techniques
Authors: Wolfgang Ahrendt, Jonas Becker-Kupczok, Simon Bliudze, Petra van den Bos, Marco Eilers, Gidon Ernst, Martin Fabian, Paula Herber, Marieke Huisman, Raúl E. Monti, Robert Rubbens, Larisa Safina, Jonas Schiffl, Alexander J. Summers, Mattias Ulbrich, Alexander Weigl
This repository contains the material of the Casino case study. In this paper we discuss several specification solutions. In particular you find the following solutions:
- [uppaal] -- Timed automata
- [supervisory] --
- [tlaplus] -- Classical model-checking
- [solc-verify] -- Code-based Verification based on Verification Condition
- [secc] -- Deductive Verification
- [vercors] -- Deductive Verification
- [javabip] --
- [2vyper] -- Deductive verification with resource-based specifications