2 papers
cs.PL2026
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…
cs.LO2025
Bisimilarity in fresh-register automata
Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order…