大发棋牌www官方网址入口-主页欢迎您

11月2日:Stefano Tonetta研究员
发布时间:2022-10-24

报告题目: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.



华东师范大学大发棋牌www官方网址入口

www.sei.ecnu.edu.cn Copyright Software Engineering Institute

办公邮箱:office@sei.ecnu.edu.cn | 院办电话:021-62232550 | 学院地址:上海中山北路3663号理科大楼