Seminars with Caterina Urban,
Erika Ábrahám and Anna Becchi  

26 September 2025 | Aula Stringa - Online | 13:30 | Caterina Urban (Inria & École Normale Supérieure, Université PSL, Paris, France), Erika Ábrahám (RWTH Aachen University, Germany) and Anna Becchi (FBK-FM, Trento, Italy) 

Program:

1:30-2:30 pm | Caterina Urban, Termination Resilience Static Analysis

2:30-3:30 pm | Erika Ábrahám,  On the idea of exploration-guided satisfiability checking

3:30-4:15 pm | Anna Becchi, Syntactically Convex Model-Based Projection for Linear Rational Arithmetic


Erika Ábrahám

Title: On the idea of exploration-guided satisfiability checking

Abstract

Satisfiability checking is a research area devoted to the development and implementation of algorithms for the automated satisfiability check of logical formulas.

SAT solving for propositional logic became impressively powerful due to an elegant combination of a smart search space exploration and proof construction. This idea has been later generalized to quantifier-free first-order logic formulas over some theories, most notably quantifier-free real algebra, in the framework of the model constructing satisfiability calculus (MCSAT). Both approaches are based on the generalization of "wrong guesses" made by the exploration into pieces of a proof, which are collected and used to synthesize a global proof during the solving process. While being one of the currently best approaches, for large or complex formulas, a large number of "proof pieces" cause high effort for their processing and thus restrict scalability.

Thus the question comes up whether there are ways to store such information in a more structured way, which requires lower costs for processing. This thought is taken up by the method of the cylindrical algebraic coverings, developed for the satisfiability check of conjunctions of polynomial constraints.
In this talk, we will discuss the above ideas and methods, and highlight their relations and differences.

Bio

Erika Ábrahám (RWTH Aachen University, Germany) https://ths.rwth-aachen.de/people/erika-abraham/
Erika Ábrahám was born in Hungary and moved to Germany to study Computer Science at the University of Kiel. She received her Ph.D. from the University of Leiden, the Netherlands in 2005, for her work on deductive roof systems for concurrent programs. As a postdoctoral researcher, she was active in different areas of formal methods at the University of Freiburg and at Forschungszentrum Jülich, before she became professor at RWTH Aachen University, Germany in 2008. Her research areas cover the development of algorithms and tools (solvers) for satisfiability checking, and formal methods for the synthesis and analysis of discrete, hybrid, and probabilistic systems.

Caterina Urban
Title: Termination Resilience Static Analysis
Abstract
We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., controlled) variables. Our framework is a semantic generalization of Cousot and Cousot's abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné's decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. Our approach is implemented in an open-source tool and evaluated on benchmarks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities.
Bio
Caterina is a research scientist in the Inria research team ANTIQUE (ANalyse StaTIQUE), working on static analysis methods and tools to enhance the reliability and our understanding of data science and machine learning software. She is Italian and studied for her Bachelor’s (2009) and a Master’s (2011) degree in Computer Science at the University of Udine. She then moved to France and completed her Ph.D. (2015) in Computer Science, working under the supervision of Radhia Cousot and Antoine Miné at École Normale Supérieure. Before joining Inria (2019), she was a postdoctoral researcher at ETH Zurich in Switzerland.


Anna Becchi
Title: Syntactically Convex Model-Based Projection for Linear Rational Arithmetic
Abstract
Quantifier elimination (QE) is a key task in formal verification algorithms. An important feature of QE is the ability to return partial results when interrupted early: a notable example is Model-Based Projection (MBP), a technique used to return an under-approximation of QE. Another desirable feature of QE is that the output is returned in a concise representation. In the theory of Linear Rational Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity, that is, they return a disjunction even for a conjunctive input, or they return a large non-minimal representation. This can disadvantage the QE client. To address these issues, we introduce the new concept of Bidirectional Model-Based Projection (BMBP). Given a model, BMBP returns both an over- and an under-approximation of QE. We define a new QE algorithm for LRA (BMBP-QE) that (i) is an anytime algorithm capable of providing two complementary partial results -- a conjunctive over-approximation and a disjunctive under-approximation -- when interrupted early, (ii) returns a minimal conjunction when the input is conjunctive, and (iii) applies to arbitrary LRA formulae. Given the twofold nature of the partial results, BMBP has the potential to enable new strategies in verification algorithms currently relying on MBP. We show that our algorithm does not introduce significant overhead compared to QE methods using MBP. In fact, BMBP-QE outperforms SMT-based QE algorithms, offering improvements in both runtime and result size.
Bio
Anna Becchi is a Computer Science PhD candidate at Fondazione Bruno Kessler in Trento, Italy, focusing on reverse engineering and verification of cyber-physical systems in collaboration with the Italian Railway Network.
Her past work involved abstract interpretation in the domain of convex polyhedra, applied to both static analysis and hybrid systems verification.
Her current research interests include SMT-based invariant checking and CHC solving.