BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:40ee2d9b-1f4d-45e5-849e-14c45801bc7a
X-WR-CALNAME:[MTV] - Nicola Gigante (Free University of Bozen-Bolzano) - Te
 mporal Logics Modulo Theories for Infinite-State Verification
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20221030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20231029T030000
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:40ee2d9b-1f4d-45e5-849e-14c45801bc7a
DTSTAMP:20260428T210053Z
CLASS:PUBLIC
DESCRIPTION:Linear Temporal Logic (LTL) is one of the most common formalism
 s for expressing\nproperties of systems in formal verification and other f
 ields. However\, its\npropositional nature limits its applicability to fin
 ite-state systems\, whereas\nmany interesting scenarios often require reas
 oning in an infinite-state\nsettings. Indeed\, many formalisms and techniq
 ues have been proposed in the last\ndecades to specify and verify infinite
 -state systems. This talk presents our\ntake at the problem. We recently i
 ntroduced LTL Modulo Theories (LTLMT)\, a\nfirst-order extension of LTL th
 at provides both a general and expressive\ntheoretical framework to reason
  about infinite-state specification and\nverification\, and encouraging ea
 rly experimental evidence of its applicability\,\nthanks to the ability to
  exploit efficient off-the-shelf Satisfiability Modulo\nTheories solvers. 
 After introducing the necessary background and defining LTLMT\,\nwe will g
 o through early results in the area\, and explore current directions\,\nre
 cent results and many future developments.
DTSTART;TZID=Europe/Paris:20231019T130000
DTEND;TZID=Europe/Paris:20231019T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] - Nicola Gigante (Free University of Bozen-Bolzano) - Tempora
 l Logics Modulo Theories for Infinite-State Verification
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
