Open-World Assertion Checking for Smart Contracts via Game Semantics

Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos

We present a game semantics framework for open-world safety analysis of Ethereum smart contracts. We model the interaction between a contract and its environment as a two-player ga…