State-Transition Systems for Smart Contracts
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Contracts
Core
Heaps
Libs
.gitignore
LICENSE
Makefile
Makefile.coq
README.md
_CoqProject

README.md

Smart Contract as Automata

State-Transition Systems for Smart Contracts: semantics and properties.

Building Instructions

Requirements

We recommend installing the requirements via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Building the project

make clean; make

Project Structure

  • Core/Automata2.v - definition of the automata-based language semantics;
  • Contracts/Puzzle.v - a simple puzzle-solving game contract and its properties;
  • Contracts/Crowdfunding.v - the Crowdfunding contract and its properties;