Programming Languages
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java…
The ubiquity of accelerators in high-performance computing has driven programming complexity beyond the skill-set of the average domain scientist. To maintain performance portability in the future, it is imperative to decouple…
This paper presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such…
Remora is a higher-order, rank-polymorphic array-processing programming language, in the same general class of languages as APL and J. It is intended for writing programs to be executed on parallel hardware. We provide an example-driven…
We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of…
We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that allow inferring the gas consumption associated to selected…
In this paper, we propose a new paradigm for program optimization which is based on aggressive aggregation, i.e., on a partial evaluation-based decomposition of acyclic program fragments into a pair of computationally optimal structures: an…
The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more…
We present a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various…
Managing resources---file handles, database connections, etc.---is a hard problem. Debugging resource leaks and runtime errors due to resource mismanagement are difficult in evolving production code. Programming languages with static type…
Semantic subtyping enables simple, set-theoretical reasoning about types by interpreting a type as the set of its values. Previously, semantic subtyping has been studied primarily in the context of statically typed languages with structural…
We study the first-order probabilistic programming language introduced by Staton et al. (2016), but with an additional language construct, $\mathbf{stat}$, that, like the fixpoint operator of Atkinson et al. (2018), converts the description…
We present new operational semantics for serverless computing that model the event-driven relationships between serverless functions, as well as their interaction with platforms services such as databases and object stores. These semantics…
The goal of this paper is to help mainstream programmers routinely use formal verification on their smart contracts by 1) proposing a new YAML-format for writing general-purpose formal specifications, 2) demonstrating how a formal…
Abstract interpretation is a general framework for expressing static program analyses. It reduces the problem of extracting properties of a program to computing an approximation of the least fixpoint of a system of equations. The de facto…
We review some results regarding specification, programming and verification of different classes of distributed systems which stemmed from the research of the Concurrency and Mobility Group at University of Firenze. More specifically, we…
This paper presents the design and implementation of Juniper: a functional reactive programming language (FRP) targeting the Arduino and related microcontroller systems. Juniper provides a number of high level features, including parametric…
We present GOOL, a Generic Object-Oriented Language. It demonstrates that a language, with the right abstractions, can capture the essence of object-oriented programs. We show how GOOL programs can be used to generate human-readable,…
Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art…
Smart contracts on a blockchain behave precisely as specified by their code. A vulnerability in this code can lead to unexpected behaviour, which is hard to fix because a blockchain does not allow to change smart contract code after its…