6 citations · 8 across the 15 of their papers we have counts for
21 papers
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Louis Rustenholz, Alessio Mansutti, Pedro López-García +3
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate r…
Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
Louis Rustenholz, Manuel V. Hermenegildo, Pedro Lopez-Garcia +3
We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the f…
How (and when) can you fit examples to logic-based hypothesis classes over infinite structures?
Michael Benedikt, Alessio Mansutti
We study fitting problems, sometimes called ``training problems'', where we have a finite sample consisting of inputs and outputs, and we want to know whether there is a function i…
MCSAT Modulo Transcendental Arithmetics
Jorge Gallego-Hernández, Enrico Lipparini, Alessio Mansutti
We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and…
Optimization Modulo Integer Linear-Exponential Programs
S Hitarth, Alessio Mansutti, Guruprerana Shabadi
This paper presents the first study of the complexity of the optimization problem for integer linear-exponential programs which extend classical integer linear programs with the ex…
One-Parametric Presburger Arithmetic has Quantifier Elimination
Alessio Mansutti, Mikhail R. Starchak
We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function , where is a…
On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number
Jorge Gallego-Hernández, Alessio Mansutti
This paper investigates , that is the extension of the existential theory of the reals by an additional unary predicate for the…
Integer Linear-Exponential Programming in NP by Quantifier Elimination
Dmitry Chistikov, Alessio Mansutti, Mikhail R. Starchak
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer line…
On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
Christoph Haase, Alessio Mansutti, Amaury Pouly
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that…
Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)
Luca Geatti, Alessio Mansutti, Angelo Montanari
This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish…
Integer Programming with GCD Constraints
Rémy Defossez, Christoph Haase, Alessio Mansutti +1
We study the non-linear extension of integer programming with greatest common divisor constraints of the form , where and are linear polynomials, is a…
The complexity of Presburger arithmetic with power or powers
Michael Benedikt, Dmitry Chistikov, Alessio Mansutti
We investigate expansions of Presburger arithmetic, i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function…
Notes on kAExp(pol) problems for deterministic machines
Alessio Mansutti
The complexity of several logics, such as Presburger arithmetic, dependence logics and ambient logics, can only be characterised in terms of alternating Turing machines. Despite qu…
Presburger arithmetic with threshold counting quantifiers is easy
Dmitry Chistikov, Christoph Haase, Alessio Mansutti
We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier that determines whether the nu…
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
Bartosz Bednarczyk, Stéphane Demri, Raul Fervari +1
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic…
A Complete Axiomatisation for Quantifier-Free Separation Logic
Stéphane Demri, Étienne Lozes, Alessio Mansutti
We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no ex…
Internal Calculi for Separation Logics
Stéphane Demri, Etienne Lozes, Alessio Mansutti
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal…
The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
Stéphane Demri, Etienne Lozes, Alessio Mansutti
The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of add…
Loose Graph Simulations
Alessio Mansutti, Marino Miculan, Marco Peressotti
We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern m…
Deciding Hedged Bisimilarity
Alessio Mansutti, Marino Miculan
The spi-calculus is a formal model for the design and analysis of cryptographic protocols: many security properties, such as authentication and strong confidentiality, can be reduc…
Distributed execution of bigraphical reactive systems
Alessio Mansutti, Marino Miculan, Marco Peressotti
The bigraph embedding problem is crucial for many results and tools about bigraphs and bigraphical reactive systems (BRS). Current algorithms for computing bigraphical embeddings a…