Room 206 (2nd floor, badged access)
12 octobre 2023 - 14h00
Temporal Logics Modulo Theories for Infinite-State Verification
par Nicola Gigante de Free University of Bozen-Bolzano, Italy
Abstract: Linear Temporal Logic (LTL) is one of the most common formalisms for expressing
properties of systems in formal verification and other fields. However, its
propositional nature limits its applicability to finite-state systems, whereas
many interesting scenarios often require reasoning in an infinite-state
settings. Indeed, many formalisms and techniques have been proposed in the last
decades to specify and verify infinite-state systems. This talk presents our
take at the problem. We recently introduced LTL Modulo Theories (LTLMT), a
first-order extension of LTL that provides both a general and expressive
theoretical framework to reason about infinite-state specification and
verification, and encouraging early experimental evidence of its applicability,
thanks to the ability to exploit efficient off-the-shelf Satisfiability Modulo
Theories solvers. After introducing the necessary background and defining LTLMT,
we will go through early results in the area, and explore current directions,
recent results and many future developments.
Nicola Gigante got his PhD in Computer Science at the University of Udine, Italy, in 2019,
and is now a Researcher at the Free University of Bozen-Bolzano, Italy. His research can
be located at the border between formal verification and symbolic artificial intelligence,
with a particular focus on temporal reasoning, including verification and reactive synthesis
from temporal specifications, and temporal planning. He intends to candidate for a CNRS position at VERIMAG.
