形式化方法与应用论坛

---

形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已成为安全攸关系统质量保障不可或缺的重要载体。形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面己显示出无可取代的潜力。

ChinaSoft 2021形式化方法与应用Track围绕形式化方法基础理论、技术、支持工具以及领域应用等展开，重点关注形式化方法在人工智能、区块链、量子计算等新兴领域内的研究成果，以及创新性理论技术在行业内的示范应用。

论坛组织委员会：

陈立前（国防科技大学）

孙 猛（北京大学）

日程安排：

时间：2021年12月24日（星期五），14:00~18:00

   2021年12月25日（星期六），10:40~12:30

论坛议程：

论坛组织委员会简介：

1. 论坛主席：陈立前

简介： 陈立前，国防科技大学计算机学院副教授。主要从事程序分析与验证、抽象解释相关研究。在ACM/IEEE Transactions、POPL、FSE等期刊会议上发表论文60余篇，获ACM SIGSOFT杰出论文奖，出版教材译著3部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。

2. 论坛主席：孙猛

简介： 孙猛，北京大学数学科学学院信息与计算科学系教授，博士生导师，中国计算机学会形式化方法专委会委员，中国工业与应用数学学会区块链专委会委员，曾任职于荷兰数学与计算机科学研究中心（CWI）、新加坡国立大学、联合国大学国际软件技术研究所（UNU-IIST），主要研究领域为程序理论、软件形式化方法。主持及作为主要成员参加国家及省部级项目十余项，在IEEE Transactions on Software Engineering、Theoretical Computer Science、ICSE、ESEC/FSE、AAAI、FM等期刊及会议发表论文百余篇，获TASE 2015、SBMF 2017等多个国际会议最佳论文奖，任ICFEM 2018等国际会议程序委员会主席，FM 2019、TACAS 2019等多个国际会议程序委员会委员。