VELOCiTY

The Verification, Logic, Concurrency, and Types Group

The VELOCiTY Research Group within the Department of Computer Science at University of Malta combines theoretical advances with tool development to bring foundational ideas into practice. Our work draws from concurrency theory, runtime monitoring, and programming languages, with the aim of developing rigorous verification methodologies that address the challenges of building reliable modern systems.

Recent publications

Conference papers

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation in OOPSLA 2025

Radosław Jan Rowicki, Adrian Francalanza, Alceste Scalas
If At First You Don't Succeed: Extended Monitorability through Multiple Executions in LICS 2025

Antonis Achilleos, Adrian Francalanza, Jasmine Xuereb
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory in CONCUR 2025

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen
A Theory of (Linear-Time) Timed Monitors in ECOOP 2025

Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, Adrian Francalanza
Centralized vs Decentralized Monitors for Hyperproperties in CONCUR 2024

Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, Jana Wagemaker
COTS: Connected OpenAPI Test Synthesis for RESTful Applications in COORDINATION 2024

Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, Emilio Tuosto

Source
Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax) in COORDINATION 2024

Adrian Francalanza, Gerard Tabone, Frank Pfenning

Extended Version • Source
Runtime Instrumentation for Reactive Components in ECOOP 2024

Luca Aceto, Duncan Paul Attard, Adrian Francalanza, Anna Ingólfsdóttir

Distinguished artefact • Extended Version • Technical Report • Artefact

Journal papers

Grits: A message-passing programming language based on the semi-axiomatic sequent calculus in Sci. Comput. Program.

Adrian Francalanza, Gerard Tabone, Frank Pfenning
Complexity results for modal logic with recursion via translations and tableaux in Log. Methods Comput. Sci.

Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Anna Ingólfsdóttir
On first-order runtime enforcement of branching-time properties in Acta Informatica

Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir
ElixirST: A session-based type system for Elixir modules in J. Log. Algebraic Methods Program.

Adrian Francalanza, Gerard Tabone
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties in Log. Methods Comput. Sci.

Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir

Tools

Grits

Source

Grits is a type-checker and interpreter for intuitionistic session types written in Go, based on the semi-axiomatic sequent calculus

ElixirST

Source

ElixirST (Session Types in Elixir) applies session types to a fragment of the Elixir language

detectEr

Source • Project page

A runtime verification tool for monitoring asynchronous component systems

SeTTS

Source

Automated Test Generation for RESTful APIs

Projects

ESERCS

Enhanced Safety for Equipment Remote Control System

The project aims to develop a modular proof-of-concept monitoring system for shopfloors that ensures safety by disabling hazardous machines when violations occur, while avoiding unnecessary disruptions and supporting flexible, plug-and-play reconfiguration.

Funding Important Projects of Common European Interest (IPCEI)

MoVeMnt

Mode(l)s of Verification and Monitorability

The MoVeMnt project investigates the theoretical and practical foundations of monitorability, focusing on hyperproperties, structured verdicts, resource-augmented monitors, complexity and decidability, and their relation to other verification techniques.

Funding The Icelandic Centre for Research (RANNIS)

BehAPI

Behavioural Application Program Interfaces

The project aims to integrate prototype behavioural type tools into mainstream programming languages and development frameworks used in industry.

Funding H2020 Research, innovation and science policy experts (RISE)

TheoFoMon

Theoretical Foundations for Monitorability

The project aims to advance the theoretical foundations of monitorability in variants of Hennessy-Milner logic with recursion, extending prior work to stricter detection conditions, alternative instrumentation, real-time systems, enforceability, and ultimately a prototype tool for runtime analysis.

Funding The Icelandic Centre for Research (RANNIS)

SecBAPI

Behavioural APIs for enhanced Security

This project investigates the applications of Behavioural Types to express and verify security properties of API-based software via techniques such as static typechecking and runtime monitoring.

Funding University of Malta Research Excellence Fund

Group members

Current

Duncan Paul Attard	Postdoctoral researcher
Caroline Cucciardi	PhD student
Adrian Francalanza	Professor
Marietta Galea	PhD student
Gerard Tabone	PhD student
Gianluca Zahra	PhD student
Jasmine Xuereb	PhD student

Former

Christian Bartolo Burlò	PhD graduate
Ian Cassar	PhD graduate