題目：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最佳論文獎。