定理证明理论与应用论坛

---

随着计算机系统在工业和生活中越来越广泛的应用，软件和硬件的可靠性受到越来越多的关注。定理证明方法将程序和系统的正确性表达为数学命题，然后使用逻辑推导的方式证明正确性。不同于基于程序测试的方法，定理证明能保证覆盖所有分支情况，完全排除一个特定类型的错误。而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小的限制，验证非常复杂的系统和性质。因此，定理证明技术不仅是形式化方法领域，也是众多其他应用领域国内外学者的关注焦点和研究新热点。

近年来，定理证明已经逐步用于越来越多的软件、硬件系统验证，这一方面为软硬件系统的安全性保障提供了新的有力工具，另一方面也成为定理证明技术发展的有利契机。目前，定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要，对于分析、逻辑、概率等基础定理证明库或求解方案的需求也越来越迫切。

ChinaSoft2021“定理证明理论与应用”论坛的主题将围绕定理证明方法的各项应用，包括其在数学定理验证、算法数据结构验证、编译器验证、操作系统验证以及混成系统建模等各个方面的实际应用，征集国内外研究人员在定理证明及相关领域的突破性技术、关键理论以及重要应用，并探讨其未来的发展前景。

论坛组织委员会：

曹钦翔（上海交通大学）

詹博华（中科院软件所）

赵永望（浙江大学）

日程安排：

时间：2021年12月24日（星期五），08:30~12:30

论坛议程：

论坛组织委员会简介：

1. 论坛主席：曹钦翔

简介： 曹钦翔，上海交通大学副教授，其长期从事基于定理证明的程序验证与程序逻辑研究，其主要参与的VST项目是目前为止较为成熟的用于验证C程序的工具。另外，曹钦翔还参与撰写了Coq定理证明教材《Software Foundations》的第五卷。

2. 论坛主席：詹博华

简介： 詹博华，中科院软件所副研究员，其主要研究方向是交互式定理证明，关注证明自动化方法和工具设计，以及嵌入式系统的建模和验证。在Isabelle定理证明器中开发了auto2证明自动化工具，应用于基于集合论的形式化数学和基于分离逻辑的程序验证。此外，参与开发了量子程序验证工具QHLProver。目前正在开发HolPy交互式定理证明器。

3. 论坛主席：赵永望

简介： 赵永望，浙江大学 教授/博士生导师，移动终端安全浙江省工程实验室主任，工信部重大专项首席科学家，中国计算机学会(CCF)杰出会员。担任ARINC653国际操作系统标准委员会委员、CCF系统软件专委会和形式化方法专委会委员、国际标准化组织 ISO/IEC JTC1 SOA研究组组长等。主要研究方向包括形式逻辑与验证、操作系统安全、编程语言原理等。主持和参与国家自然基金重点项目、工信部重大专项、载人航天工程重点项目等二十余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。