Manuel Di Agostino

Manuel Di Agostino

PhD student in Mathematics

PhD student in Mathematics at the University of Parma, part of the joint doctoral program with the Universities of Modena-Reggio Emilia and Ferrara. My research is in Software Verification: I design sound static analyses based on Abstract Interpretation for multilanguage Rust/C codebases, targeting memory safety in hybrid safety-critical systems.

I earned my Master’s degree in Computer Science at the University of Parma, where I worked on static analysis of the R programming language, developing a parametric abstract domain for R vectors.

Latest updates

Starting my PhD in Mathematics at the University of Parma (joint program with the Universities of Modena-Reggio Emilia and Ferrara), working on sound static analysis of hybrid Rust/C codebases.

Selected as an artifact reviewer for VMCAI 2027.

Selected publications

see all →
WORK
WORK Pinned publication

Towards Statically Reasoning About R Vectors

We present a parametric abstract domain for R vectors that captures vector lengths, element values, and attributes, implemented on top of the flowR static analysis framework.

Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, Matthias Tichy
NSAD 2026 (to appear)
DOI
Abstract
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. We present a parametric abstract domain for R vectors, defined over μR, a core calculus designed to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. We define abstract operators for all μR operations, equip the domain with a widening operator to ensure termination, and implement it on top of flowR, a static analysis framework for R, evaluating it on a suite of 61 handcrafted programs covering six categories of vector operations.

Career highlights

see CV →