CCF ChinaSoft 2023 论坛巡礼 | CCF-华为胡杨林基金-形式化方法专项（海报）论坛-编程知识

2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办，将于2023年12月1-3日在上海国际会议中心举行。

本次大会主题是“智能化软件创新推动数字经济与社会发展”，学术、工业、教育、竞赛等分论坛活动40余场，期待您的参与！

目前大会火热报名中！

CCF ChinaSoft 2023官方首页：

http://chinasoft.ccf.org.cn/

点击文末“阅读原文”或扫描下方二维码进入官方注册通道:

https://conf.ccf.org.cn/chinasoft2023

✦ +

论坛巡礼

论坛名称

CCF-华为胡杨林基金-形式化方法专项（海报）论坛

时间

2023年12月2日（星期六），14:00 – 18:00

地点

上海国际会议中心，5楼廊厅

论坛简介

“CCF-华为胡杨林创新基金”是由华为与中国计算机学会联合发起，致力于为海内外高校及科研院所的学者搭建产学研合作及学术交流的平台。本次研讨会邀请了获得2023年“CCF-华为胡杨林创新基金”形式化方法专项资助的优秀学者进行项目进展介绍及技术交流，旨在进一步明确项目的方案、技术与应用场景，加强学术界与工业界合作，促进形式化方法与技术研究和发展。

论坛主席

Forum Chairmen

秦胜潮

华为

华为资深技术专家，形式化验证科学家。目前担任费马实验室主任，负责形式化技术研究和工程能力建设。北京大学学士（1997）和博士（2002）。博士毕业后在新加坡国立大学担任新加坡-MIT联盟计算机科学研究员。2005年起在英国Durham和Teesside大校任教，历任讲师、正教授、科研副院长等职。2021年加入华为香港研究所。主要研究领域包括软件理论与形式化方法，软件工程，程序语言等。研究工作主要涉及形式化规范和建模，程序理论和程序逻辑，程序分析与验证等。

刘关俊

同济大学

教授，博士生导师，2011年获得同济大学计算机软件与理论专业博士学位，先后于新加坡科技设计大学、德国柏林洪堡大学（德国洪堡基金资助）从事博士后研究工作，2013年进入同济大学计算机科学系工作至今。是中国计算机学会高级会员，计算机学会形式化方法专委会与软件工程专委会执行委员、中国人工智能学会会员、IEEE Senior Member、Associate Editor of IEEE Transactions on Computational Social Systems（2023.1-2025.12）。已出版学术专著4本，发表学术论文160余篇，主持国家自然科学基金、上海市曙光人才项目、上海市科技创新行动计划（人工智能专项）等项目多项。主要研究兴趣：Petri网理论、模型检测、实时嵌入式系统、强化学习与无人机协同等。

论坛嘉宾

Forum Guests

陈明帅

浙江大学

浙江大学百人计划研究员、博士生导师、启真学者，CCF形式化方法专委委员，国家优秀青年基金（海外）获得者。2019年于中国科学院软件研究所获计算机软件与理论专业博士学位，2019年至2022年于德国RWTH Aachen从事博士后研究工作。主要研究方向包括形式验证、程序理论、概率/量子系统、信息物理融合系统等，在Inf. Compt.、IEEE Trans. Automat. Contr.、OOPSLA、CAV、FM、IJCAR、TACAS等重要国际期刊或会议上发表学术论文20余篇，曾获中国科学院院长特别奖、ATVA 2018杰出论文奖、FMAC 2019最佳论文奖，曾任30余个国际期刊或会议的同行（子）审稿人，并在实时系统领域旗舰会议RTSS 2020及ESWEEK 2022上做专题报告。主持国家优秀青年科学基金项目（海外）、CCF-华为胡杨林基金形式化专项，作为项目骨干承担国家重点研发计划，参与研发的混成系统建模、分析与验证工具链MARS被成功应用于国家探月二期工程“嫦娥”三号软着陆等国家重大工程。

报告题目：

面向C代码的自适应抽象解释技术研究

报告摘要：

抽象解释是程序静态分析与验证中的核心理论，而验证准确率与执行效率之间的平衡是抽象解释技术在大规模代码级验证中所面临的关键挑战之一。Astrée、Frama-C/EVA等基于抽象解释的C/C++静态分析工具虽支持多种不同的抽象域，但其抽象域的选择与调整（精化）过程高度依赖于专家知识，导致验证过程效率低、误报率高且难以完全自动化。本项目旨在探究自适应精度的抽象解释技术，构建基于代码局部特征的抽象域自动适配方法，设计支持增量式验证的抽象域自动精化策略，研发与Frama-C框架整合的内存安全性原型验证工具，实现高效、低误报、高度自动化的C程序代码级形式化验证。

李晖

北京邮电大学

副教授，博导，CCF高级会员，形式化方法/计算机安全/信息保密专委委员，主要研究方向：安全协议和移动安全。承担国自然基金委海外联合基金、国家重大专项、重点研发计划等多项国家科研项目，主持中兴产学研、SONY公司等多项校企合作项目。在NDSS、TDSC和ESORICS等国际重要期刊和学术会议上发表50余篇论文。

报告题目：

TLS协议关键代码形式化验证技术研究

报告摘要：

为了进行 TLS 协议栈的代码级别功能验证，研究面向代码的形式化验证方法，构建TLS1.3协议标准中关键流程的形式化模型和OpenSSL中的TLS1.3协议C语言实现代码的形式化模型，验证验证密码协议的实现与标准文档的一致性，证明C语言实现代码的功能正确性。

夏壁灿

北京大学

北京大学数学科学学院教授,中国工业与应用数学学会常务理事，中国数学会计算机数学专委会副主任，CCF形式化方法专委会委员，北京大学大数据分析与应用技术国家工程实验室副主任。曾任北京大学数学科学学院副院长和信息科学系主任。主要研究方向包括符号计算，程序与混成系统验证，自动定理证明等。在实代数、实几何自动推理、程序与混成系统验证、SMT求解等多个方面取得了系列研究成果，在多个重要的学术会议和期刊上发表了80余篇论文。主持或参与了多项国家级科研项目，包括国家自然科学基金重大项目、重点项目、面上项目，科技部重点研发项目和国家973项目。近年来，主持国家基金委重点项目“面向程序验证的自动定理证明理论、方法与工具研究”、科技部国家重点研发计划“数学和应用研究”专项课题“面向安全攸关系统安全性验证的数学理论和分析方法”。

报告题目：

基于局部搜索的C程序断言判定方法与工具

报告摘要：

在数字化的时代，确保软件的正确性是构建可靠系统的基石，软件的正确性是建立值得信赖的系统的核心。采用形式化方法验证软件的正确性是确保软件的可靠性的核心方法。本项目拟利用约束求解和局部搜索技术，评估程序是否能安全地到达预期状态（具体的状态是代码中ASCL描述的断言），旨在研发一种启发式、高效的程序状态断言判定技术。

黄宇

南京大学

博士，教授，博士生导师，主要研究领域为系统软件与软件工程，具体研究内容包括分布式算法、分布式系统、轻量级形式化方法等。在ACM PODC、IEEE TC、IEEE TPDS等国际会议与期刊上发表学术论文多篇。主持与参与国家自然科学基金等多项国家级科研项目。2014年获南京大学登峰人才支持计划资助，2018年入选首届高校计算机专业优秀教师奖励计划，协助指导的博士论文获得2016、2017年度中国计算机学会优秀博士论文奖，建设了南京大学“百层次”优质课程《算法设计与分析》，编写的教材入选2020年度南京大学“十三五”规划教材。

报告题目：

分布式系统深层缺陷检测技术研究

报告摘要：

交换机平台控制面监控路由通路变化，然后将路由配置信息发送到数据转发面，转发面基于新的配置信息进行实际的数据包转发。控制面中的各个模块之间具有较高的独立性，并通过套接字通信进行交互，模块间的数据存储管理方式，已经由传统的独立存储变成了基于共享数据库的存储。交换机平台功能模块间的数据共享方式与业务协同方式，导致在高并发场景下各模块间围绕共享数据库的协同可能会出现分布式时序问题。这类分布式时序问题在常规测试环境中难以发现，但它们在高并发、长时间的系统执行中又必将暴露，并引发较为严重的后果。面向交换机操作系统的分布式时序问题与传统并发编程领域的数据竞争问题有相似之处，但是又有一些重要的区别。一方面，交换机平台底层的共享资源是数据库，它不仅提供了数据表供上层模块读写，还提供了一些同步功能。这与传统并发编程中共享内存地址的读写有所不同。另一方面，交换机平台的功能模块间通过共享数据库的协同都是基于底层的套接字通信实现的。基于上述分析，我们将借鉴经典并发编程领域数据竞争问题的建模和解决方案，针对交换机平台的特点，对分布式时序问题进行抽象建模并研究针对性的解决方案。

刘关俊

同济大学

报告题目：

基于Petri网的Rust 程序并发安全漏洞检测

报告摘要：

Rust 是一种系统编程语言，其以安全、并发和高效为设计目标，在多个领域都有着广泛应用。研究表明，Rust已知的内存错误大都来自于Unsafe代码，现有的工作对于Unsafe代码的检测仅针对如整数溢出等典型安全漏洞，可扩展性不强，不能覆盖整个生态系统，特别是对并发造成的错误。由于Rust的编译器保证的安全性范围有限，Unsafe代码和指针的传递，可能会造成数据竞争、双重锁定等并发错误；另外，静态分析在逻辑错误，如死锁、并发时序错误上存在漏报误报等问题。本项目基于Petri网进行Rust程序并发安全漏洞检测，对死锁、数据竞争和异步时序问题分别构造相应的Petri网模型，实现从Rust程序（中间代码）到相应Petri网模型的自动抽取，以及在相应模型上自动检测死锁、数据竞争、异步时序问题，降低误报率和错报率。

姚培森

浙江大学

浙江大学研究员、博导，国家级青年人才，CCF形式化专委委员，ACM SIGPLAN会员。主要研究方向程序分析与验证、程序合成、自动定理证明，相关成果在编程语言(PLDI, OOPSLA)、软件工程(ESEC/FSE, ICSE， ASE, ISSTA, TOSEM)、信息安全(S&P, USENIX Security, TDSC)等领域发表CCF-A会议/期刊论文20余篇，入选OOPSLA杰出论文奖、Google Research Paper Rewards等奖项; 针对约束求解、抽象解释和CFL可达性等基础算法提出系列优化方法，应用于大规模真实程序的动静态缺陷检测，发现Linux 内核等开源软件数百真实缺陷、获得近百CVE ID，成果部署在蚂蚁、华为等公司。担任相关领域顶级会议(PLDI, ISSTA, RAID, EuroS&P)程序委员会委员，以及ACM TOPLAS, ACM TKDD, IEEE TR, ATVA, ESEC/FSE, ASE, VMCAI等期刊和会议审稿人。详情见rainoftime.github.io

报告题目：

最优化模理论(OMT)约束求解算法研究

报告摘要：

最优化模理论(Optimization Modulo Theory, OMT)是SMT的一种扩展问题: 给定逻辑约束P和目标函数f(X), 计算P的一个可满足解，使得目标函数f的取值最大/最小。OMT求解在程序分析与验证中有重要应用，比如最优抽象解释、WCET(worst case execution time)分析等。然而, OMT求解相对于SMT求解通常具有更高的复杂度。目前OMT求解主要包括两类方法：将OMT转换成其他自动推理问题（如Weighted MaxSAT)，以及基于SMT的迭代式优化算法（如线性搜索）。然而在处理复杂约束时，现有方法仍面临性能问题，限制了其在大规模软件分析中的应用。本项目面向软硬件验证中广泛使用的位向量约束，研究基于portfolio方法以及divide-and-conquer方法的并行OMT求解算法，以提升OMT求解的可扩展性，并为并行约束求解提供新的思路和方法。

陈哲

南京航空航天大学

陈哲，南京航空航天大学计算机科学与技术学院副教授。博士毕业于法国国立应用科学院，主要研究兴趣包括形式化方法、软件验证、程序分析等。主持国家自然科学基金3项（青年基金、民航联合基金、面上项目）等。作为第一作者在TSE、SPE、COMPJ、IPL、FUIN等著名国际学术期刊和ICSE、ISSTA、TACAS、SPIN、COMPSAC、ICFEM、TASE等著名国际会议共发表了60余篇研究论文，并获得2019年ACM SIGSOFT杰出论文奖。

报告题目：

SCADE同步语言程序模型检测器研究与实现

报告摘要：

安全关键嵌入式软件开发领域的事实标准开发工具SCADE Suite是“卡脖子”产品之一，研发SCADE Suite软件的国产替代解决方案、实现自主可控刻不容缓。而SCADE Suite中最重要的模块之一就是形式化验证模块，但是目前没有针对SCADE的开源模型检测器，这为实现SCADE Suite的自主可控带来了更大的挑战。为了解决SCADE程序模型检测器的国产替代问题、实现自主可控，同时解决传统的串行模型检测存在的性能较差的问题，提出基于SMT求解器的SCADE程序并行模型检测方法，并依此实现一款新的SCADE程序模型检测器。

汪宇霆

上海交通大学

上海交通大学John Hopcroft计算机科学中心副教授，此前于美国耶鲁大学计算机系担任博士后研究员，博士毕业于美国明尼苏达大学双城分校计算机系。长期从事形式化方法方面研究，内容涵盖形式化验证和程序设计语言的理论基础（包括证明论、类型论、逻辑框架等）以及它们在关键性系统软件（如编译器和操作系统）中的应用，代表性研究成果发表于形式化验证和程序设计语言的国际顶会（如POPL、CAV、OOPSLA、ESOP等）。此外，还致力于开发基于证明论的定理证明工具，作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具Abella（http://abella-prover.org），其已被成功应用于程序设计语言学术界的多个研究项目。

报告题目：

Rust核心语言机制的编译验证方法

报告摘要：

编译器是关键性的系统软件，形式化验证可以在逻辑层面保证编译器不存在任何漏洞，因此备受关注。现有编译器验证方法只适用于传统的命令式和函数式编程语言，无法有效支持Rust语言的新特性以及它们引起的编译器复杂性。本项目的目标是提出新型的编译器验证方法，以支持1）Rust所有权机制和2）Safe/Unsafe Rust的分离编译。本项目的形式化开发将基于交互式定理证明工具Coq完成。通过本项目的研究，我们将得到一套支持Rust关键语言特性的可组合编译器验证方法，突破已有编译器验证方法无法支持Rust语言的瓶颈。

葛存菁

南京大学人工智能学院

南京大学人工智能学院博士后。2019年于中国科学院软件研究所获得博士学位，后前往奥地利林茨大学从事博士后工作。主要研究方向为反绎学习、约束的可满足性问题与约束的解计数问题。在人工智能与理论计算机科学的知名会议期刊（IJCAI、IJCAR、TCS等）发表论文十余篇。曾获得研究生国家奖学金，入选2021年南京大学“毓秀学者计划”。

报告题目：

SMT(LA)约束的解计数方法研究与工具实现

报告摘要：

SMT(LA)约束的解计数问题已是自动推理领域中的热点研究问题，在程序分析中有大量应用，但是相较于可满足性问题的求解，对于解计数问题的研究尚不充分。其中以线性算术约束为基础的SMT(LA)约束解计数问题，实用化的方法与工具较少，已提出的算法的性能依然常无法满足实际应用的需要。本项目将围绕线性算数约束和 SMT(LA)约束，研究如何实现已有的约束解计数算法，并针对实际问题（如程序分析）进行改进，从而建立高性能的SMT(LA)约束解计数工具集。