专刊论坛

约束求解与定理证明论坛

2022年11月25日(8:30-12:30)



论坛简介

约束求解与定理证明论坛是中国软件大会的一个专刊论坛,是促进约束求解与定理证明两方面发展的学术交流平台。该论坛具体关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用。论坛包括1个特邀报告和8个常规报告。其中,新加坡理工大学助理教授David Sanan博士为我们带来关于Web 3形式化验证方法的特邀报告。常规报告来自《软件学报》约束求解与定理证明专刊的投稿论文,本次论坛挑选了其中8篇论文,邀请作者到论坛进行报告。

📢 【腾讯会议号】  546502638
📢 【直播链接】【点击观看视频直播】
📢 【B站直播】【点击观看B站直播】

论坛日程

时间 报告题目 讲者/嘉宾
08:30-09:10 特邀报告:Formal Methods for the Web3 David Sanan
09:10-09:30 论文报告:L4虚拟内存子系统的形式化验证 章乐平
09:30-09:50 论文报告:GCMCR:基于有向图构建约束的并发缺陷检测方法 李硕川
09:50-10:10 论文报告:基于精化的TrustZone多安全分区建模与形式化验证 曾凡浪
10:10-10:20 休息
10:20-10:40 论文报告:基于不可满足核的近似逼近可达性分析 于忠祺
10:40-11:00 论文报告:针对教学场景的ZFC集合论Coq形式化 万新熠
11:00-11:20 论文报告:基于目标制导符号执行的智能合约安全漏洞检测方法 杨慧文
11:20-11:40 论文报告:LLRB算法的函数式建模及其自动验证 黄志鹏
11:40-12:00 论文报告:强表达描述逻辑本体的后继式公理定位研究 李静

论坛嘉宾




1.论坛嘉宾:David Sanan(Singapore Institute of Technology)

报告题目:Formal Methods for the Web3

摘要: Web3.0, also known as Web3, is the latest iteration of the World Wide Web and introduces concepts such as decentralisation, blockchain, and token-based economics. While potentially providing increased data security, scalability, and privacy, some of its inherent features, like blockchain immutability and public software interfaces to Decentralized Finance, are sources of countless attacks with billions of dollars lost as a consequence. Formal methods have appeared as a practical solution to partially identify and detect vulnerable software on different layers of the Web3. However, methodologies adopted by the Web3 industry may not be enough to cope with the increasing complexity of the software composing Web3. In this keynote, we will give an overview of the current state of formal methods in Web3 and what directions and problems formal methods need to follow and solve to be able to protect Web3.

简介: Dr. David Sanan is an Assistant Professor at the Singapore Institute of Technology. He received his M.S. degree in computer science and his PhD degree in Software Engineering and Artificial Intelligence from the University of Malaga, Malaga, Spain, in 2003 and 2009, respectively. His research interest covers formal methods applied to a wide number of applications going from programming language semantics to software verification. In particular, David has been working during the last years on applying formal methods to real-world applications like quantum computing, certification of smart contracts, and the verification of security micro-kernels in the Aerospace and Electric-Vehicle domain.



论坛主席





1.论坛主席:蔡少伟(中国科学院软件研究所)

简介: 蔡少伟,中科院软件所研究员、博导、中科院优秀导师,获得国家优秀青年基金资助。主要研究约束求解、组合优化以及EDA(电子设计自动化)验证工具。在命题逻辑可满足性问题(SAT)、可满足性模理论(SMT)问题、最大可满足性问题(MaxSAT)等国际比赛多次获得冠军,在国际EDA比赛获得亚军;提出可满足性问题的混合搜索方法,解决了命题逻辑推理与搜索方向十大挑战的第7个挑战,获得SAT会议最佳论文奖。他研发的约束求解器已成功应用于电子设计自动化(EDA)和软件验证、云计算故障检测等工业场景。相关成果发表在CAV,ICSE,IJCAI,CP,SAT等会议和Artificial Intelligence、IEEE Trans. Computers等期刊上。






2.论坛主席:陈振邦(国防科技大学)

简介: 陈振邦,国防科技大学计算机学院博士/副教授、硕士生导师,CCF形式化方法专委执行委员,NASAC青年创新奖获得者。近年来,主要围绕符号执行相关的理论、技术和应用开展研究,成果发表在ICSE、FSE、ISSTA、ASE、FM、TCS等重要国际会议或期刊上,获CCF A类会议ACM SIGSOFT杰出论文奖2次。负责承担国家自科基金面上项目2项、重点项目子课题1项、青年项目1项以及其他类型省部级课题多项,作为主要骨干参与国家重大研究项目多项。获国家科技进步二等奖1项、省部级科技进步二等奖2项。研制的程序分析工具在多个国家重大工程中开展应用,为解决国家重大工程中的软件质量保障问题探索了有效解决途径。






3.论坛主席:王戟(国防科技大学)

简介: 王戟,国防科技大学计算机学院教授,博士生导师 ,国家杰出青年科学基金获得者,教育部长江学者奖励计划特聘教授。主要从事可信、智能和新兴软件系统研究。先后承担了国家自然科学基金重点、国际合作重点、重大研究计划项目,国家863、973和重点研发计划项目等课题,获国家科技进步二等奖。现担任CCF形式化方法专委会主任、中国工程院院刊FITEE执行副主编、IEEE Software AE和软件学报领域编委等职。






4.论坛主席:詹博华(中国科学院软件研究所)

简介: 詹博华的研究方向是形式化方法。2014年博士毕业于普林斯顿大学数学系,之后在麻省理工学院和慕尼黑工业大学任博士后。2018年加入中科院软件所,现任副研究员。主要工作包括证明自动化方法和交互式定理证明器的设计与实现,嵌入式系统的建模与验证方法,以及在程序验证、操作系统、分布式系统、量子程序验证的应用。在CAV, IJCAR/CADE, TACAS, ITP, J. Automated Reasoning等形式化方法领域的主要会议和期刊发表文章30余篇。






5.论坛主席:赵永望(浙江大学)

简介: 赵永望,浙江大学,教授、博士生导师,移动终端安全浙江省工程研究中心主任,工信部重大专项首席科学家,CCF杰出会员,CCF系统软件专委、形式化方法专委和抗恶劣计算专委执行委员,国际ARINC653操作系统标准委员会成员等。主要研究方向为形式化验证、系统安全、编程语言等,主持和参与工信部重大专项、国家自然基金重点项目、载人航天工程重点项目、浙江省尖兵计划项目等二十余项,获省部级科技进步一等奖2项。相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。提出了操作系统形式验证的系统性理论和方法,已应用到十多个国产操作系统和国外工业/开源操作系统中,显著提升国产系统的安全可靠性。