时间：2020年11月11日晚上7：30-8:30

　　地点：信息工程学院大会议室

　　主讲人：姜宇 & 詹博华

　　主讲人简介：

　　姜宇，清华大学软件学院副教授,博士生导师。重点关注人工智能、工控等领域的软件安全，利用深度学习与模糊测试等技术，进行软件缺陷的自动挖掘与理解。相关工具在广泛使用的系统软件中累积发现500余个缺陷，其中125个漏洞（例如操作系统Linux-kernel 漏洞 CVE-2019-7707 和工控协议Lib-iec61850 漏洞 CVE-2018-19121）被收录入美国国家信息安全漏洞库。相关成果以第一作者或通讯作者在Security, ASE,TSE等会议和期刊上发表论文50余篇，并获ACM EMSOFT，ICSE-SEIP等会议的最佳论文或提名奖5次。

　　詹博华， 中科院软件所计算机科学重点实验室副研究员。研究方向是交互式定理证明里的证明自动化，以及在形式化数学和程序验证里的应用。2014年从普林斯顿大学数学系获得博士学位。博士期间的研究方向是低维拓扑学。2014-2017在麻省理工学院数学系任博士后。2017-2018在慕尼黑工业大学任博士后。现在研究成果发表于ITP, TACAS, 和IJCAR国际会议。

　　主讲内容简介：

　　主题1：模型驱动的软件开发工具Tsmart-GalsBlock.

　　简介：工业控制软件的实现方式异构和行为空间爆炸两大特性，导致其安全保障效率低，效果差。 首先，实现方式异构，会导致构造失据，工控软件不仅有C程序实现，还有VHDL等程序的实现，统一的描述构造和功能安全保障难。其次，行为空间爆炸会导致测试失信，工控软件不仅要和用户交互，还需要和设备，环境进行交互，完备的测试分析和信息安全保障难。本报告主要针对软件安全保障展开，针对大规模软件开发运维过程中面临的复杂异质异构问题，提出基于异构形式化模型的可信构造方法，提升功能安全性。介绍模型驱动的开发工具Tsmart-GalsBlock，支持同步异构嵌入式系统的模型驱动的设计，集成了当前主流建模工具支持工具的特征，融入了C和VHDL的协同代码生成的特征。

　　主题2: Verified interactive computation of definite integrals

　　简介: Symbolic computation is involved in many proof in mathematics, as well as derivations and analysis of systems in science and engineering. Performing these computations in computer algebra systems is relatively simple, but there is no guarantee for the correctness of the answers. In contrast, verifying computations in interactive theorem provers provides much stronger guarantees of correctness, but requires more time and expertise. In this paper, we describe a general architecture for combining the advantages of these two methods, and demonstrate it on the computation of definite integrals.