8 papers
Software is infrastructure: failures, successes, costs, and the case for formal verification
Giovanni Bernardi, Adrian Francalanza, Marco Peressotti +1
In this chapter we outline the role that software has in modern society, along with the staggering costs of poor software quality. To lay this bare, we recall the costs of some of…
Proceedings of the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification
Giorgio Bacci, Adrian Francalanza
This volume contains the proceedings of GandALF 2025, the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification. GandALF 2025 took place on 16-17th…
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
RadosÅaw Jan Rowicki, Adrian Francalanza, Alceste Scalas
Many software applications rely on concurrent and distributed (micro)services that interact via message-passing and various forms of remote procedure calls (RPC). As these systems…
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
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 pr…
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…
If At First You Don't Succeed: Extended Monitorability through Multiple Executions
Antonis Achilleos, Adrian Francalanza, Jasmine Xuereb
This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited t…