3 citations · 6 across the 13 of their papers we have counts for
13 papers
A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
Daragh King, Vasileios Koutavas, Laura Kovacs
Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, ye…
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…
LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
Daragh King, Vasileios Koutavas, Laura Kovacs
The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The gener…
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 CCS to CSP: the m-among-n Synchronisation Approach
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield
We present an alternative translation from CCS to an extension of CSP based on m-among-n synchronisation (called CSPmn). This translation is correct up to strong bisimulation. Unli…
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…
Locally Nameless Permutation Types
Edsko de Vries, Vasileios Koutavas
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is…
Distinguishing between Communicating Transactions
Vasileios Koutavas, Maciej Gazda, Matthew Hennessy
Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical…
A Safety and Liveness Theory for Total Reversibility (Extended Abstract)
Claudio Antares Mezzina, Vasileios Koutavas
We study the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollbacks lead the systems to past states. Similar to previous work on…
Type-Based Analysis for Session Inference
Carlo Spaccasassi, Vasileios Koutavas
We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop…
Towards Efficient Abstractions for Concurrent Consensus
Carlo Spaccasassi, Vasileios Koutavas
Consensus is an often occurring problem in concurrent and distributed programming. We present a programming language with simple semantics and build-in support for consensus in the…