27 citations · 47 across the 17 of their papers we have counts for
18 papers
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…
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…
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…
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos +1
This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and…
Higher-Order Bounded Model Checking
Yu-Yang Lin, Nikos Tzevelekos
We present a Bounded Model Checking technique for higher-order programs. The vehicle of our study is a higher-order calculus with general references. Our technique is a symbolic st…
Trace Properties from Separation Logic Specifications
Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber +2
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Se…
Higher-Order Linearisability
Andrzej S. Murawski, Nikos Tzevelekos
Linearisability is a central notion for verifying concurrent libraries: a given library is proven safe if its operational history can be rearranged into a new sequential one which,…
Block structure vs scope extrusion: between innocence and omniscience
Andrzej S. Murawski, Nikos Tzevelekos
We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation…
Trace semantics for polymorphic references
Guilhem Jaber, Nikos Tzevelekos
We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal inter…
Runtime Verification Based on Register Automata
Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen +1
We propose TOPL automata as a new method for runtime verification of systems with unbounded resource generation. Paradigmatic such systems are object-oriented programs which can dy…
History-Register Automata
Radu Grigore, Nikos Tzevelekos
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (H…
A System-Level Semantics
Dan R. Ghica, Nikos Tzevelekos
Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rul…
Introduction to Categories and Categorical Logic
Samson Abramsky, Nikos Tzevelekos
The aim of these notes is to provide a succinct, accessible introduction to some of the basic ideas of category theory and categorical logic. The notes are based on a lecture cours…
Full abstraction for nominal general references
Nikos Tzevelekos
Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects.…