IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2023 > Temporal Logics Modulo Theories for Infinite-State Verification
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Nicola Gigante

miércoles 8 de noviembre de 2023

11:00am 302-Mountain View and Zoom4 (, password:@s3)

Nicola Gigante, researcher, 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.