4 papers
On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them
Rob van Glabbeek, Daniele Gorla, Myrthe Spronck
In the literature on mutual exclusion, bounded bypass has been used for a long time as a strengthening of starvation-freedom, but, to the best of our knowledge, it still lacks a sa…
Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Stian Lybech, Daniele Gorla, Luca Aceto
This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The…
A Sound Type System for Secure Currency Flow
Luca Aceto, Daniele Gorla, Stian Lybech
In this paper we focus on TinySol, a minimal calculus for Solidity smart contracts, introduced by Bartoletti et al. We start by rephrasing its syntax (to emphasise its object-orien…
Centralized vs Decentralized Monitors for Hyperproperties
Luca Aceto, Antonis Achilleos, Elli Anastasiadi +3
This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end…