Report title: Temporary Satisfaction Modular Topics

Report time: 16:00 on November 2nd

Conference number: 353444734 (Microsoft Teams)

Host: Li Jianwen

Abstract:

Checking temporal satisfiability (or validity) is a fundamental problem to make formal verification scale up with compositional reasoning. In this talk, we focus on LTL satisfiability modulo theories, which generalizes the satisfiability problem for LTL to the first-order case with respect to some background theories. Compositional reasoning takes into account both synchronous and asynchronous interactions of components. Temporal satisfiability is defined uniformly with discrete and (super) dense models of time. We show how these problems are solved via SMT-based model checking and applied to various benchmarks.

Introduction of Lectuer:

Stefano Tonetta is head of the Embedded Systems Unit of the Digital Industry Center of FBK. He received the PhD form the University of Trento in 2006. His interests focus on formal methods for safety critical systems. He co-authors more than ninety papers with various contributions to SMT-based model checking and temporal logics for software, hybrid systems, or architectural design models.