4 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…
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…
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…