Alessio Mansutti


I am an Assistant Professor at the IMDEA Software Institute. Previously, I was a Research Associate in the Automated Verification Group of the University of Oxford. I hold a PhD degree from ENS Paris-Saclay, where I was a student of Stéphane Demri and Étienne Lozes in the Laboratoire Spécification et Vérification.

Below, you will find a summary of current and past projects. All my papers are available here.

Hey, I'm currently looking for motivated internship (and future PhD?) students. Email me if you are interested!

Advanced Reasoning in Arithmetic Theories

the star

The goal of the ERC project ARiAT is to advance the state-of-the-art in decision procedures for expressive arithmetic theories, improve complexity bounds and push the decidability frontier of extensions of arithmetic theories with counting and non-linear operations. See here for more information.

Reachability Predicates in Separation Logic

the star

The goal of this project is to study the complexity and expressiveness of separation logics featuring reachability predicates. Separation logic is a mathematical formalism for reasoning about pointer programs. Among the various features of this logic, reachability predicates have a special status, as they allow to express crucial properties of the memory such as acyclicity and garbage-freedom.

Modal Logics with Composition Operators

the star

The goal of this project is to develop a framework of modal logics featuring different forms of frame composition that are heavily inspired by the logic of Bunched Implications. By relying on standard techniques from finite model theory, we study the expressiveness and computational complexity of our logics, and compare them with more standard formalisms (e.g. graded modal logic).

Internal Calculi for Spatial Logics

the star

The goal of this project is to design internal axiomatisations for spatial logics such as separation logics and ambient logics. Designing an internal (a.k.a. Hilbert-style) axiomatisation for your favourite logic is usually quite challenging. It does not lead necessarily to optimal decision procedures, but the completeness proof usually provides essential insights to better understand the logic at hand, and develop better abstractions that can improve the performances of tools.