6 papers
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…
Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory
Luca Aceto, Antonis Achilleos, Duncan Paul Attard +4
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its executio…
Typing Composite Subjects
Luca Aceto, Daniele Gorla, Stian Lybech
Many type systems have been presented in the literature for variants of the pi-calculus, but none of them are able to handle composite subjects such as those found in the language…
Preventing Out-of-Gas Exceptions by Typing
Luca Aceto, Daniele Gorla, Stian Lybech +1
We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend T…
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…