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, Stephan Merz, 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] -- Nonblocking verification
- [tlaplus] -- State machine specification with model checking
- [solc-verify] -- Source-level deductive verification
- [secc] -- Deductive verification
- [vercors] -- Deductive verification
- [javabip] -- Deductive verification of component-based systems
- [2vyper] -- Deductive verification with resource-based specifications