13:00
14:00

[MTV] - Nicola Gigante (Free University of Bozen-Bolzano) - Temporal Logics Modulo Theories for Infinite-State Verification

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.

salle 178, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159