arXiv subjects

Daniele Gorla

Publications and source records attributed to Daniele Gorla.

At least 19 recordsLinked to original sources

arXiv2026

An Incremental Algorithm for Checking the Possibility of Braess Paradox in Dynamic Nets

Braess paradox is a well-known phenomenon that originates when latency at Wardrop equilibrium in traffic networks decreases because of removing edges. The possibility of having the paradox was called vulnerability by Roughgarden in 2006 and was characterized later on by graph-theoretical notions, both for undirected and for directed graphs. In this paper we provide an algorithm for the incremental case of checking vulnerability for dynamically evolving graphs. The crucial idea to keep the amortized cost linear for every edge addition is that we do not need to run the vulnerability algorithm on the whole graph, but only on a well-identified subgraph, determined by the edge that we are adding. Overall, to add m edges, we pay a cost of O(m2); this aligns with the O(m2) cost of the state-of-the-art static algorithm for vulnerability.

cs.GT↗

arXiv2026

On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them

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 satisfying definition as a liveness property on its own. Moreover, we have encountered MUTEX protocols for which this notion needs to be slightly weakened in order to be met. To solve these issues, we first provide a formal definition of bounded bypass (that also corrects a previous definition from Raynal) and then introduce the notions of post-doorway and intermittent bounded bypass, two liveness properties that lie between starvation-freedom and bounded bypass. Essentially, intermittent bounded bypass weakens bounded bypass by ignoring the possible bypasses that may happen during the execution of a certain finite set of write operations to shared registers. Orthogonally, post-doorway bounded bypass ignores the bypasses that may happen during a finite initial phase of the lock protocol. Furthermore, we study an algorithm proposed by Yoah Bar-David in 1998 to enhance the liveness properties of any deadlock-free MUTEX protocol and prove that: (1) in the setting of atomic registers, this algorithm upgrades any deadlock-free mutual exclusion protocol to a bounded bypass one, with a bound that is quadratic in the number of processes; and (2) in the setting of safe and regular registers, the very same algorithm ensures the intermittent version of bounded bypass, still with a quadratic (but slightly different) bound. Finally, we provide logical formulae for the different notions of bounded bypass defined in this paper and use them to confirm all claims made here, by using model checking. This had a positive impact on the theoretical development of the work, since it allowed us to identify and correct small mistakes/ambiguities in definitions and proofs.

cs.DC↗

arXiv2026

Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts

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 idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided 'proof certificate' of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack.

cs.PL↗

arXiv2025

A Sound Type System for Secure Currency Flow

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-oriented flavour) and give a new big-step operational semantics. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system for noninterference and show that well-typed programs satisfy call integrity as well; hence, programs that are accepted by our type system satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.

cs.PL↗

arXiv2025

Denotational Semantics for Probabilistic and Concurrent Programs

We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas semantics for concurrent or randomized programs in isolation is well studied, their combination has not been thoroughly explored and presents unique challenges. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution cannot be captured by straightforward generalizations of prior work on pomsets and convex languages, prominent models for those effects, individually. Our model has good domain theoretic properties, important for semantics of unbounded loops. We also prove two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism.

cs.PL↗

arXiv2025

Centralized vs Decentralized Monitors for Hyperproperties

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, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.

cs.LO↗

arXiv2025

CUBETESTERAI: Automated JUnit Test Generation using the LLaMA Model

This paper presents an approach to automating JUnit test generation for Java applications using the Spring Boot framework, leveraging the LLaMA (Large Language Model Architecture) model to enhance the efficiency and accuracy of the testing process. The resulting tool, called CUBETESTERAI, includes a user-friendly web interface and the integration of a CI/CD pipeline using GitLab and Docker. These components streamline the automated test generation process, allowing developers to generate JUnit tests directly from their code snippets with minimal manual intervention. The final implementation executes the LLaMA models through RunPod, an online GPU service, which also enhances the privacy of our tool. Using the advanced natural language processing capabilities of the LLaMA model, CUBETESTERAI is able to generate test cases that provide high code coverage and accurate validation of software functionalities in Java-based Spring Boot applications. Furthermore, it efficiently manages resource-intensive operations and refines the generated tests to address common issues like missing imports and handling of private methods. By comparing CUBETESTERAI with some state-of-the-art tools, we show that our proposal consistently demonstrates competitive and, in many cases, better performance in terms of code coverage in different real-life Java programs.

cs.SE↗

arXiv2024

Typing Composite Subjects

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 epi, which features polyadic synchronisation. The purpose of this paper is to address the question of how to type composite subjects in a general fashion. We assess the validity of our proposal by first proving the standard correctness results for a type system (i.e., subject reduction and type safety). Then, we follow the path opened by Sangiorgi in 1998 and show an encoding in epi of a minimal OO language called WC (While with \Classes) whose ``expectable'' type system exactly corresponds to the one induced by ours via the encoding. This comparison contributes to understanding the relationship between our types and conventional types for OO languages.

cs.PL↗

arXiv2024

Preventing Out-of-Gas Exceptions by Typing

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 TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.

cs.PL↗

arXiv2024

An implicit function theorem for the stream calculus

In the context of the stream calculus, we present an Implicit Function Theorem (IFT) for polynomial systems, and discuss its relations with the classical IFT from calculus. In particular, we demonstrate the advantages of the stream IFT from a computational point of view, and provide a few example applications where its use turns out to be valuable.

cs.LO↗

arXiv2024

BaBE: Enhancing Fairness via Estimation of Latent Explaining Variables

We consider the problem of unfair discrimination between two groups and propose a pre-processing method to achieve fairness. Corrective methods like statistical parity usually lead to bad accuracy and do not really achieve fairness in situations where there is a correlation between the sensitive attribute S and the legitimate attribute E (explanatory variable) that should determine the decision. To overcome these drawbacks, other notions of fairness have been proposed, in particular, conditional statistical parity and equal opportunity. However, E is often not directly observable in the data, i.e., it is a latent variable. We may observe some other variable Z representing E, but the problem is that Z may also be affected by S, hence Z itself can be biased. To deal with this problem, we propose BaBE (Bayesian Bias Elimination), an approach based on a combination of Bayes inference and the Expectation-Maximization method, to estimate the most likely value of E for a given Z for each group. The decision can then be based directly on the estimated E. We show, by experiments on synthetic and real data sets, that our approach provides a good level of fairness as well as high accuracy.

cs.LG↗

arXiv2023

On the (Im)Possibility of Estimating Various Notions of Differential Privacy

We analyze to what extent final users can infer information about the level of protection of their data when the data obfuscation mechanism is a priori unknown to them (the so-called ''black-box'' scenario). In particular, we delve into the investigation of two notions of local differential privacy (LDP), namely ε-LDP and Rényi LDP. On one hand, we prove that, without any assumption on the underlying distributions, it is not possible to have an algorithm able to infer the level of data protection with provable guarantees; this result also holds for the central versions of the two notions of DP considered. On the other hand, we demonstrate that, under reasonable assumptions (namely, Lipschitzness of the involved densities on a closed interval), such guarantees exist and can be achieved by a simple histogram-based estimator. We validate our results experimentally and we note that, on a particularly well-behaved distribution (namely, the Laplace noise), our method gives even better results than expected, in the sense that in practice the number of samples needed to achieve the desired confidence is smaller than the theoretical bound, and the estimation of ε is more precise than predicted.

cs.CR↗

arXiv2021

DOCTOR: A Simple Method for Detecting Misclassification Errors

Deep neural networks (DNNs) have shown to perform very well on large scale object recognition problems and lead to widespread use for real-world applications, including situations where DNN are implemented as "black boxes". A promising approach to secure their use is to accept decisions that are likely to be correct while discarding the others. In this work, we propose DOCTOR, a simple method that aims to identify whether the prediction of a DNN classifier should (or should not) be trusted so that, consequently, it would be possible to accept it or to reject it. Two scenarios are investigated: Totally Black Box (TBB) where only the soft-predictions are available and Partially Black Box (PBB) where gradient-propagation to perform input pre-processing is allowed. Empirically, we show that DOCTOR outperforms all state-of-the-art methods on various well-known images and sentiment analysis datasets. In particular, we observe a reduction of up to $4\%$ of the false rejection rate (FRR) in the PBB scenario. DOCTOR can be applied to any pre-trained model, it does not require prior information about the underlying dataset and is as simple as the simplest available methods in the literature.

cs.CV↗

arXiv2021

Algebra and coalgebra of stream products

We study connections among polynomials, differential equations and streams over a field K, in terms of algebra and coalgebra. We first introduce the class of (F,G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial of the streams themselves and their derivatives. Our first result is that, for every (F,G)-product, there is a canonical way to construct a transition function on polynomials such that the induced unique final coalgebra morphism from polynomials into streams is the (unique) K-algebra homomorphism -- and vice versa. This implies one can reason algebraically on streams, via their polynomial representation. We apply this result to obtain an algebraic-geometric decision algorithm for polynomial stream equivalence, for an underlying generic (F,G)-product. As an example of reasoning on streams, we focus on specific products (convolution, shuffle, Hadamard) and show how to obtain closed forms of algebraic generating functions of combinatorial sequences, as well as solutions of nonlinear ordinary differential equations.

cs.FL↗

arXiv2019

Conflict vs Causality in Event Structures

Event structures are one of the best known models for concurrency. Many variants of the basic model and many possible notions of equivalence for them have been devised in the literature. In this paper, we study how the spectrum of equivalences for Labelled Prime Event Structures built by Van Glabbeek and Goltz changes if we consider two simplified notions of event structures: the first is obtained by removing the causality relation (Coherence Spaces) and the second by removing the conflict relation (Elementary Event Structures). As expected, in both cases the spectrum turns out to be simplified, since some notions of equivalence coincide in the simplified settings; actually, we prove that removing causality simplifies the spectrum considerably more than removing conflict. Furthermore, while the labeling of events and their cardinality play no role when removing causality, both the labeling function and the cardinality of the event set dramatically influence the spectrum of equivalences in the conflict-free setting.

cs.LO↗

arXiv2019

Approximate Model Counting, Sparse XOR Constraints and Minimum Distance

The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is based on the idea of using random XOR constraints to, roughly, successively halving the solution set until no model is left: this is checked by invocations to a SAT solver. The effectiveness of this procedure hinges on the ability of the SAT solver to deal with XOR constraints, which in turn crucially depends on the length of such constraints. We study to what extent one can employ sparse, hence short, constraints, keeping guarantees of correctness. We show that the resulting bounds are closely related to the geometry of the set of models, in particular to the minimum Hamming distance between models. We evaluate our theoretical results on a few concrete formulae. Based on our findings, we finally discuss possible directions for improvements of the current state of the art in approximate model counting.

cs.LO↗

arXiv2017

A Polynomial-time Algorithm for Detecting the Possibility of Braess Paradox in Directed Graphs

A directed multigraph is said vulnerable if it can generate Braess paradox in Traffic Networks. In this paper, we give a graph-theoretic characterisation of vulnerable directed multigraphs; analogous results appeared in the literature only for undirected multigraphs and for a specific family of directed multigraphs. The proof of our characterisation also provides an algorithm that checks if a multigraph is vulnerable in O(|V| |E|^2); this is the first polynomial time algorithm that checks vulnerability for general directed multigraphs. The resulting algorithm also contributes to another well known problem, i.e. the directed subgraph homeomorphism problem without node mapping, by providing another pattern graph for which a polynomial time algorithm exists.

cs.DS↗

arXiv2016

Graph Theoretic Investigations on Inefficiencies in Network Models

We consider network models where information items flow %are sent from a source to a sink node. We start with a model where routing is constrained by energy available on nodes in finite supply (like in Smartdust) and efficiency is related to energy consumption. We characterize graph topologies ensuring that every saturating flow under every energy-to-node assignment is maximum and provide a polynomial-time algorithm for checking this property. We then consider the standard flow networks with capacity on edges, where again efficiency is related to maximality of saturating flows, and a traffic model for selfish routing, where efficiency is related to latency at a Wardrop equilibrium. Finally, we show that all these forms of inefficiency yield different classes of graphs (apart from the acyclic case, where the last two forms generate the same class). Interestingly, in all cases inefficient graphs can be made efficient by removing edges; this resembles a well-known phenomenon, called Braess's paradox.

cs.DM↗