-
A Logic For Fresh Labelled Transition Systems
Authors:
Mohamed H Bandukara,
Nikos Tzevelekos
Abstract:
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can capture fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn are one of the simplest classes of history-dependent automa…
▽ More
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can capture fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn are one of the simplest classes of history-dependent automata operating on infinite input alphabets. Each automaton comes equipped with a finite set of registers where it can store data values and compare them with others from the input. In addition, the automaton can accept an input just if it be fresh: not seen in the computation before. The logic we introduce can express a variety of properties, such as the existence of an infinite path of distinct data values or the existence of a finite path where some taint property is violated. We study the model checking problem and its complexity via reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
△ Less
Submitted 17 June, 2025;
originally announced June 2025.
-
An Operational Semantics for Yul
Authors:
Vasileios Koutavas,
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
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 that is congruous with the literature of programming languages, lends itself to language proofs, and can serve as a precise, widely accessible specification for the language. Our two semantics stay faithful to the origin…
▽ More
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 that is congruous with the literature of programming languages, lends itself to language proofs, and can serve as a precise, widely accessible specification for the language. Our two semantics stay faithful to the original, informal specification of the language but also clarify under-specified cases such as void function calls. Our presentation allows us to prove the equivalence between the two semantics. We also implement the small-step semantics in an interpreter for Yul which avails of optimisations that are provably correct. We have tested the interpreter using tests from the Solidity compiler and our own. We envisage that this work will enable the development of verification and symbolic execution technology directly in Yul, contributing to the Ethereum security ecosystem, as well as aid the development of a provably sound future type system.
△ Less
Submitted 1 July, 2024;
originally announced July 2024.
-
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
Authors:
Vasileios Koutavas,
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
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 Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms…
▽ More
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 Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that reach bounded configurations but can potentially have unbounded call stacks and input an unbounded number of unknown functions from their context. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stackless Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. To enhance the effectiveness of our bisimulation, we develop up-to techniques and confirm their soundness for PDNF Bisimulation. We develop a prototype implementation of our technique which is able to verify equivalence in examples from practice and the literature that were out of reach for previous work.
△ Less
Submitted 2 November, 2023;
originally announced November 2023.
-
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
Authors:
Vasileios Koutavas,
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotiening, the LTS constructs traces corresponding to interactions wi…
▽ More
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotiening, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCF$_{\textsf{v}}$ program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.
△ Less
Submitted 2 October, 2023;
originally announced October 2023.
-
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
Authors:
Vasileios Koutavas,
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-comple…
▽ More
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.
△ Less
Submitted 22 October, 2021; v1 submitted 6 May, 2021;
originally announced May 2021.
-
Bisimilarity in fresh-register automata
Authors:
Andrzej S. Murawski,
Steven J. Ramsay,
Nikos Tzevelekos
Abstract:
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 to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have…
▽ More
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 to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.
△ Less
Submitted 5 February, 2025; v1 submitted 13 May, 2020;
originally announced May 2020.
-
Symbolic Execution Game Semantics
Authors:
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
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 we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external…
▽ More
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 we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the K framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.
△ Less
Submitted 20 February, 2020;
originally announced February 2020.
-
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Authors:
Emanuele De Angelis,
Grigory Fedyukovich,
Nikos Tzevelekos,
Mattias Ulbrich
Abstract:
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 Synthesis (HCVS), which took place in Prague, Czech Republic on 6th and 7th April, respectively, as affiliated workshops of ETAPS.
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 Synthesis (HCVS), which took place in Prague, Czech Republic on 6th and 7th April, respectively, as affiliated workshops of ETAPS.
△ Less
Submitted 8 July, 2019;
originally announced July 2019.
-
Higher-Order Bounded Model Checking
Authors:
Yu-Yang Lin,
Nikos Tzevelekos
Abstract:
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 state syntactical translation based on SMT solvers, adapted to a setting where the values passed and stored during computation can be functions of arbitrary order. We prove that our algorithm is sound, and devise an optimi…
▽ More
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 state syntactical translation based on SMT solvers, adapted to a setting where the values passed and stored during computation can be functions of arbitrary order. We prove that our algorithm is sound, and devise an optimisation based on points-to analysis to improve scalability. We moreover provide a prototype implementation of the algorithm with experimental results showcasing its performance.
△ Less
Submitted 5 April, 2018;
originally announced April 2018.
-
Trace Properties from Separation Logic Specifications
Authors:
Lars Birkedal,
Thomas Dinsdale-Young,
Guilhem Jaber,
Kasper Svendsen,
Nikos Tzevelekos
Abstract:
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. Separation logic with abstract predicates enforces a resource discipline that constrains when and how calls may be made between a client and a library. Intuitively, this can enforce a protocol on the interaction trace. Thi…
▽ More
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. Separation logic with abstract predicates enforces a resource discipline that constrains when and how calls may be made between a client and a library. Intuitively, this can enforce a protocol on the interaction trace. This intuition is broadly used in the separation logic community but has not previously been formalised. We provide just such a formalisation. Our approach is based on using wrappers which instrument library code to induce execution traces for the properties under examination. By considering a separation logic extended with trace resources, we prove that when a library satisfies its separation logic specification then its wrapped version satisfies the same specification and, moreover, maintains the trace properties as an invariant. Consequently, any client and library implementation that are correct with respect to the separation logic specification will satisfy the trace properties.
△ Less
Submitted 9 February, 2017;
originally announced February 2017.
-
Higher-Order Linearisability
Authors:
Andrzej S. Murawski,
Nikos Tzevelekos
Abstract:
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, in addition, satisfies a given specification. Linearisability has been examined for libraries in which method arguments and method results are of ground type, including libraries parameterised with such methods. In this…
▽ More
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, in addition, satisfies a given specification. Linearisability has been examined for libraries in which method arguments and method results are of ground type, including libraries parameterised with such methods. In this paper we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. We use this generalised notion to show correctness of several higher-order example libraries.
△ Less
Submitted 25 October, 2016;
originally announced October 2016.
-
Block structure vs scope extrusion: between innocence and omniscience
Authors:
Andrzej S. Murawski,
Nikos Tzevelekos
Abstract:
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 with block-allocated storage through soundness, finite definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storag…
▽ More
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 with block-allocated storage through soundness, finite definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage as well as that with dynamic memory allocation. For example, we can show that dynamic variable allocation can be replaced with block-allocated variables exactly when the term involved (open or closed) is of base type and that block-allocated storage can be replaced with purely functional computation when types of order two are involved. To illustrate the restrictive nature of block structure further, we prove a decidability result for a finitary fragment of call-by-value Idealized Algol for which it is known that allowing for dynamic memory allocation leads to undecidability.
△ Less
Submitted 16 August, 2016; v1 submitted 8 May, 2016;
originally announced May 2016.
-
Trace semantics for polymorphic references
Authors:
Guilhem Jaber,
Nikos Tzevelekos
Abstract:
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 interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure…
▽ More
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 interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.
△ Less
Submitted 14 August, 2016; v1 submitted 26 February, 2016;
originally announced February 2016.
-
Runtime Verification Based on Register Automata
Authors:
Radu Grigore,
Dino Distefano,
Rasmus Lerchedahl Petersen,
Nikos Tzevelekos
Abstract:
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 dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administ…
▽ More
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 dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administers a finite-state machine with boundedly many input-storing registers. We show that TOPL automata are equally expressive to register automata and yet suitable to express properties of programs. Compared to other runtime verification methods, our technique can handle a class of properties beyond the reach of current tools. We show in particular that properties which require value updates are not expressible with current techniques yet are naturally captured by TOPL machines. On the practical side, we present a tool for runtime verification of Java programs via TOPL properties, where the trade-off between the coverage and the overhead of the monitoring system is tunable by means of a number of parameters. We validate our technique by checking properties involving multiple objects and chaining of values on large open source projects.
△ Less
Submitted 20 January, 2015; v1 submitted 24 September, 2012;
originally announced September 2012.
-
History-Register Automata
Authors:
Radu Grigore,
Nikos Tzevelekos
Abstract:
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 (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of o…
▽ More
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 (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
△ Less
Submitted 29 March, 2016; v1 submitted 4 September, 2012;
originally announced September 2012.
-
A System-Level Semantics
Authors:
Dan R. Ghica,
Nikos Tzevelekos
Abstract:
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 rules of a game between the term (the "Proponent") and its context (the "Opponent"). In general, the richer the computational features a language has, the less constrained the rules of the semantic game. In this paper we co…
▽ More
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 rules of a game between the term (the "Proponent") and its context (the "Opponent"). In general, the richer the computational features a language has, the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realizable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.
△ Less
Submitted 21 January, 2012;
originally announced January 2012.
-
Introduction to Categories and Categorical Logic
Authors:
Samson Abramsky,
Nikos Tzevelekos
Abstract:
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 course given at Oxford over the past few years. They contain numerous exercises, and hopefully will prove useful for self-study by those seeking a first introduction to the subject, with fairly minimal prerequisites. The cove…
▽ More
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 course given at Oxford over the past few years. They contain numerous exercises, and hopefully will prove useful for self-study by those seeking a first introduction to the subject, with fairly minimal prerequisites. The coverage is by no means comprehensive, but should provide a good basis for further study; a guide to further reading is included. The main prerequisite is a basic familiarity with the elements of discrete mathematics: sets, relations and functions. An Appendix contains a summary of what we will need, and it may be useful to review this first. In addition, some prior exposure to abstract algebra - vector spaces and linear maps, or groups and group homomorphisms - would be helpful.
△ Less
Submitted 7 February, 2011;
originally announced February 2011.
-
Full abstraction for nominal general references
Authors:
Nikos Tzevelekos
Abstract:
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. Recently, nominal games have been proposed for modelling functional languages with names. These are ordinary, stateful games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games…
▽ More
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. Recently, nominal games have been proposed for modelling functional languages with names. These are ordinary, stateful games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references.
△ Less
Submitted 11 September, 2009; v1 submitted 26 July, 2009;
originally announced July 2009.
