贺飞

清华大学长聘副教授，博士生导师，CCF形式化专委会常务委员

主要研究程序验证理论、方法、工具及应用。开发了模型检测和软件验证工具，并应用于航空、航天、高铁等国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, ESEC/FSE, ASE等在内的国际重要会议和期刊上发表论文70余篇。主持和参与国家973项目、自然科学基金重大项目、科技支撑计划项目、重点研发项目等10余项。任《Theory of Computing Systems》编委，CONCUR, FMCAD, SAT, APLAS, ICECCS, SETTA等国际学术会议程序委员会委员。

赵永望

CCF杰出会员、浙江大学教授/博士生导师

担任ARINC653国际操作系统标准委员会委员、中国计算机学会(CCF)高级会员、CCF系统软件专委会和形式化方法专委会委员。曾任国际标准化组织 ISO/IEC JTC1 SOA研究组组长、新加坡南洋理工大学高级研究员。主要研究方向包括操作系统安全、形式逻辑与验证、编程语言原理等。主持和参与国家自然基金重点项目、核高基重大专项、重点研发计划等项目十余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。

左志强

南京大学计算机科学与技术系副研究员

报告题目：安全C语言设计与实现

报告摘要：进入信息时代，软件已然成为现代社会的重要基础设施。确保软件安全可信，对维护信息安全以及社会生产具有重要意义。然而随着软件功能日趋复杂，规模日益增大，软件的安全可信面临愈加严峻的挑战，如何确保大规模软件的安全性，已然成为学术界、企业及政府高度关注的课题。本次报告重点介绍我们在安全C语言设计与实现方面的工作。在已有C语言的基础上，通过增加新类型，并结合动态、静态分析及编译技术，最终在编程语言与编译器层面保证软件安全。

个人简介：于新加坡国立大学获博士学位，曾在美国加州大学欧文分校从事博士后研究。科研工作聚焦于系统软件的可信保障与优化，在系统化程序分析、软硬件协同的编译器优化设计等方面取得重要进展，创新性工作以第一和通讯作者发表在包括PLDI、OOPSLA、EuroSys、ACM TOCS等国际重要学术会议和期刊上；独立研发并开源多个系统软件分析及优化系统，并已在华为、阿里等多个企业成功实现转化与应用；担任PLDI2022、FSE2022、IEEE TSE等多个国际重要学术会议程序委员及期刊审稿人。

曹钦翔

上海交通大学约翰霍普克洛夫特计算机科学中心助理教授、博导

报告题目：从程序验证到“开发即安全”

报告摘要：交互式定理证明技术是验证程序复杂性质的重要手段，其主要思想是在现有自动化验证工具无力完成验证工作的情况下，由人提供额外信息从而辅助验证工具“理解”程序并验证其功能以及安全性。经过探索，这一程序验证技术可以嵌入程序开发环境，从而实现“开发即安全”。本报告将介绍 Verified Software Toolchain（VST）工具，该工具以交互式定理证明技术为基础，集成了学术界在程序逻辑等诸多方面的理论研究前沿成果，可用于验证复杂 C 语言程序的功能正确性与安全性，排查空指针引用漏洞、缓冲区溢出错误、并发数据访问竞争等各种问题。

个人简介：曹钦翔，本科毕业于北京大学，博士毕业于美国普林斯顿大学，188体育app官网：回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心助理教授、博导。其长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题。曹钦翔是Verified Software Toolchain（VST）工具的主要开发者之一，首次实现了从业务逻辑，到源代码开发，再到编译的全链条正确性验证。

汪宇霆

上海交通大学John Hopcroft计算机科学中心副教授