报告题目：Temporal Satisfiability Modulo Theories

报告时间：11月2日16:00

会议号： 353444734（Microsoft Teams）

主持人：李建文

报告摘要：

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.

报告人简介：

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.