理论计算机科学2018寒假讲习班（一）（SWU-RISE CS-Week 1）

为提升计算机和软件工程领域青年学者及研究生的计算机科学基础理论水平，推动理论计算机科学在工程实践和技术创新中的应用，西南大学计信院软件研究与创新中心（SWU-RISE）于2018年1月15日至1月19日举办理论计算机科学2018年第一期寒假讲习班。本期讲习班授课内容涵盖理论计算机科学中的自动机、逻辑、模型检验、进程代数等内容。授课专家及课程内容简介如下。

1.     张文辉，中科院软件所计算机科学国家重点实验室研究员，2000年入选中国科学院“引进国外杰出人才计划”。主要研究兴趣包括形式模型、数理逻辑与程序逻辑、推理与模型检测、计算机软件正确性的理论与方法，实现了基于限界正确性检查和基于不动点算法的检查离散迁移系统CTL性质的模型检测工具VERDS。

授课内容：自动机理论，时序逻辑，模型检测。具体包括：有限自动机与欧米伽自动机的基本概念和原理；自动机语言包含问题，自动机空性检查问题，以及自动机空性检查的基本算法；线性时序逻辑LTL的基本成分，语义，证明系统，以及LTL的表达能力；分支时序逻辑CTL的基本成分，语义，证明系统，以及CTL的表达能力；LTL公式到自动机的转换算法以及模型检测问题到自动机语言包含问题与自动机空性检查问题的转换；符号模型以及基于不动点算法的CTL符号模型检测和基于限界语义的CTL限界正确性检查。

2.    柳欣欣， 中国科学院软件研究所研究员，2000年入选中国科学院“百人计划”。主要研究兴趣包括：并发理论，程序设计语言语义，程序逻辑系统，程序正确性验证。

授课内容：作为操作语义的基础，我们通过一系列例子介绍如何用标号迁移系统来描述并发系统，然后介绍几个比较系统状态的等价和偏序关系，特别是互模拟等价关系，以及如何用这样的关系进行并发程序验证。我们进而介绍以CCS为代表的进程代数，学习如何在这样的代数系统中进行等式推理，并研究一点等式推理 系统本身的性质，即可靠性和完备性。接下来我们学习如何在互模拟的框架里描述计算分支特性，计算终止特性等问题。最后我们将互模拟和模态逻辑联系起来，研究刻画互模拟的模态逻辑。

3.     李广元，中国科学院软件研究所计算机科学国家重点实验室研究员。主要从事实时系统的形式化验证技术与验证工具的研究。他在国际上最早实现了时间自动机关于线性时序逻辑LTL和度量时序逻辑MTL{0,∞}的符号化模型检测工具; 他还与丹麦科学家Kim Larsen等人合作实现了加权度量时序逻辑WMTL的统计模型检测以及度量时序逻辑MTL{0,∞}的控制器合成。

授课内容：时间自动机及时间Büchi自动机的基本概念、可接受语言及基本判定性结果；时间自动机的符号化语义及可达性分析；实时逻辑，度量时序逻辑MTL及其可判定性结果； 时间Büchi自动机关于LTL和度量时序逻辑MTL{0,∞}的符号化模型检测；时间自动机模型检测工具UPPAAL与CTAV；时间博弈自动机与控制器合成；时间自动机的运行时验证及统计模型检测。

时间：2018年1月15-19日，9:00-17:40

地点：西南大学第25教学楼1320会议室

联系人：赵恒军：18302301799,   zhaohj2016@swu.edu.cn

日程：请见 http://www.swu-rise.net.cn/#/article?id=76

本次讲习班不收取注册费，食宿自理，诚邀各位参加！

                               西南大学计信院软件研究与创新中心（SWU-RISE）

                                               2018年1月8日