1 citations · 1 across the 7 of their papers we have counts for
8 papers · 1 filter
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…
An Operational Semantics for Yul
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos
We present a big-step and small-step operational semantics for Yul -- the intermediate language used by the Solidity compiler to produce EVM bytecode -- in a mathematical notation…
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos
We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on…
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF). Our model is based on a labelled transition system (LTS) that combines elem…
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations simi…
Symbolic Execution Game Semantics
Yu-Yang Lin, Nikos Tzevelekos
We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular w…