题目：Formal Verification and Zero-Knowledge Proof—--Dual Pillars for Building Trustworthy Systems

报告人：李国强

时间：2025年04月10日(周四)，09：00-10：00

会议地点：31-904

报告摘要：

Formal verification (FV) serves as a mathematically framework for ensuring the complete safety of software systems, while zero-knowledge proof (ZKP) establishes cryptographic guarantees for system privacy. This presentation outlines cutting-edge research directions, specifically focusing on: Formal verification of infinite-state systems, Zero-knowledge virtual machine (ZKVM) architectures, enabling secure computation with privacy-preserving properties, and symbiotic advancements between FV and ZK: FV methodologies enhance the reliability of ZKP systems, and ZKP, in turn, safeguards sensitive information derived from FV results.

报告人简介：

李国强博士，上海交通大学软件学院副教授，博士生导师，毕业于日本北陆先端科学技术大学院大学。中国计算机学会高级会员，形式化方法专业委员会常务委员。主要研究方向为形式化验证、程序语言理论、智能系统验证与安全。主持国家自然科学基金四项、自然科学基金重点子课题一项。已经在主流会议和知名期刊发表论文超百篇，包括OPPSLA、ASE、FSE、ICSE、CSCW等顶级会议以及TSE、TSC、TDSC 、TSMCA、TDSC、 TECS等顶级期刊。获ICSE 2020最佳论文奖。