3 citations · 6 across the 13 of their papers we have counts for
3 papers · 1 filter
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…