个人简介：“CCF-IEEE CS”青年科学家奖。博士毕业于中科院软件研究所，后任中科院自动化研究所和法国波尔多第一大学博士后。2014-2015在巴黎第七大学任访问学者。长期从事计算逻辑、自动机理论、程序验证相关研究，在知名国际会议和期刊上发表论文30余篇，如LICS、POPL、CAV、Information and Computation、IJCAR、CADE、CONCUR等。主持多项国家级项目，如“十三五”全军共用信息系统装备预先研究项目、国家自然科学基金面上项目等。任ATVA‘22程序委员会共同主席， ATVA、ICECCS、LATA、GandALF等程序委员会委员。

个人简介：国家级青年项目入选者。上海交通大学学士，美国佐治亚理工学院博士，2017-2020年于美国麻省理工学院任博士后，2020年加入北京大学。研究领域为程序设计语言和软件工程，重点为编程系统和机器学习的交叉方向。一方面，利用机器学习技术来提高程序分析等编程系统的可用性，另一方面，开发了新的程序分析和语言以提高机器学习系统的质量。工作发表在 PLDI、POPL、FSE、NeurIPS 等顶级会议上，获 PLDI'14 和 FSE'15 杰出论文奖。曾任 PLDI等国际会议程序委员会委员。

报告摘要：本报告主要介绍软硬件系统安全的概念、要求和面临的挑战，分析对比各类系统安全验证方法。然后，介绍形式化验证的技术框架，以及国内外最新的发展趋势和应用情况。最后，分析当前系统安全形式化验证面临的问题，着重讨论当前交互式验证与自动化验证的现状，得出形式化验证在自动化方面的挑战与价值。

个人简介：浙江大学 计算机科学与技术学院/网络空间安全学院 教授/博导，移动终端安全浙江省工程研究中心主任，工信部重大专项首席科学家，CCF杰出会员，CCF系统软件专委、形式化方法专委和抗恶劣计算专委执行委员。主要研究方向为系统安全、形式化验证、编程语言等，相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。

报告摘要：后摩尔定律时代，硬件趋向于异构众核，高可靠和高性能的众核并发控制技术是高效发挥众核算力的关键技术之一。ARM弱内存模型、NUMA和大小核等异构众核架构给并发控制带来了挑战和机遇。本报告将介绍华为最近在应用形式化方法构建高可靠和高性能并发控制基础库方面的一些工业实践，聚焦于同步原语和异步并发通信数据结构在现代体系结构下的设计、验证和优化技术。我们认为通过形式化验证和优化工具的有效支持，程序员有信心做更为激进的并发控制算法的设计和优化，有效提升性能的同时，提供正确性保证。

个人简介：中国科学技术大学博士，华为德国德累斯顿研究所所长，操作系统和形式化方法技术专家。2017年加入华为OS内核实验室，带领形式化验证团队从事内核设计、开发和验证工作，2019年外派德国创建德累斯顿研究所，主要研究方向是操作系统、并发理论和并发程序形式化验证，致力于将形式化方法应用于工业系统软件的开发中，在形式化方法、程序语言理论和操作系统等领域的顶会POPL、CAV、CONCUR、SOSP、ASPLOS、USENIX ATC上发表多篇论文，并获得ASPLOS’21杰出论文奖。

报告摘要：现代大规模集成电路的设计与验证离不开软件工具的辅助。形式化方法在数字集成电路逻辑验证工具中的应用主要包括等价性检查与模型检测。相比于等价性检查，模型检测受电路规模制约的问题更加明显，因此提升模型检测工具的性能是一个核心问题。一种可能的解决方案是面向应用问题分析优化算法。本次报告会介绍硬件形式化方法的一类应用场景——指令功能的形式化检查，以及对应的专用模型检测方法的研究。

个人简介：香港科技大学（广州）功能枢纽微电子学域助理教授。2015年本科毕业于上海交通大学，2021年于普林斯顿大学电子与计算机系取得博士学位，主要研究硬件领域的形式化方法应用。曾获得 2020 ACM TODAES 最佳文章奖，曾担任DAC, ChinaSoft等会议审稿人。

报告摘要：命题逻辑可满足性问题（SAT）是计算机科学的核心问题之一，也是密码分析的主要方法之一。SMT是特定背景下一阶逻辑公式可满足性问题，是对SAT的重要扩展，可以视为命题逻辑框架和背景理论如线性算术理论的结合，可以更方便的表达涉及数学理论和数据结构的约束问题。SAT和SMT是EDA和软件验证的核心引擎。本报告介绍SAT和SMT的主要方法。

个人简介：中科院优秀导师，获国家优青项目，入选智源青年科学家，长白山领军人才。北京大学博士，主要研究约束求解、组合优化。发表60多篇顶级期刊和会议论文，获AIJ近五年最受欢迎论文，SAT 2021最佳论文奖。在国际SAT比赛获8次冠军10余次亚军，获SMT比赛多个冠军，EDA Challenge亚军，3个联合逻辑奥林匹克金牌。研究成果应用于国内龙头企业的芯片验证，操作系统验证，微软云平台的故障检测和虚拟机预配置，腾讯地图调度和优化，MIT材料研究等重要项目。

报告摘要：C程序的编译验证是形式化验证领域的一个重要问题，已有工作依赖基于区块的内存模型，而该模型难以支持局部内存结构转换的模块化验证，也不能被轻易拓展以描述更复杂的内存性质，这些问题极大阻碍了C程序编译验证方法的进一步发展。为解决上述问题，我们提出了一种对传统内存模型进行抽象的方法，其关键技术是通过将内存区块抽象表述为名义名字，以移除内存状态中的全局约束。通过整合抽象内存模型和CompCert，我们实现了名为Nominal CompCert的通用C程序编译验证框架，并用模块化验证、端到端完整编译过程的正确性验证检验了该框架的有效性。

个人简介：美国明尼苏达大学博士，曾任美国耶鲁大学计算机系博士后。长期从事形式化方法研究，包括形式化验证和程序设计语言的理论基础（证明论、类型论、逻辑框架等）以及它们在关键系统软件（如编译器和操作系统）中的应用，代表性成果发表于POPL、CAV、OOPSLA、ESOP等国际顶会。并致力于开发基于证明论的定理证明工具，作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具Abella，其已被成功应用于程序设计语言学术界的多个研究项目。

报告摘要：软件程序的运行常涉及隐私相关数据，比如密码、用户个人信息等。因此，如何通过技术手段保障攻击者无法通过程序运行时的可观察信息来获取相关隐私信息已经成为国内外的研究热点。本报告将探讨运行时编译优化和多方安全计算场景中的程序隐私安全性的形式验证。

个人简介：于2013年4月获得巴黎西岱大学（原巴黎狄德罗大学）计算机科学博士学位，同年8月加入华东师范大学任讲师，2016年1月破格晋升为副研究员，于2015年分别荣获上海市“浦江人才”和上海市“晨光学者”称号。2016年8月全职加入上海科技大学信息科学与技术学院，担任tenure-track助理教授、研究员，2021年7月晋升为常任副教授。研究领域包括模型检验、程序分析与验证、系统和AI安全，已在国际一流期刊和会议发表70余篇论文，如： IEEE TSE, ACM TOSEM, CAV, ICSE, ISSTA, S&P等。

个人简介：胡振江，北京大学讲席教授、计算机学院院长。1996年在日本东京大学获得博士学位。曾担任东京大学信息理工学研究科教授和日本国立信息学研究所教授/系主任。长期从事程序设计语言和软件科学与工程的研究，曾获全日本最佳博士论文奖、日本软件科学会基础研究成就奖，被评为21世纪先驱科学家（日本科学技术振兴机构）、日本工学会会士、日本工程院院士、欧洲科学院院士、IEEE会士。

个人简介：国家杰出青年科学基金获得者。南京大学数学学士、计算机硕士，中国科学院软件研究所博士。研究形式化方法，实时、嵌入式、混成系统，程序验证等。任《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《软件学报》、《电子学报》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如FM 2021）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文100多篇，出版专著2部，编著4部。