題目：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.

　　報告人簡介：

　　李國強博士,，上海交通大學(xué)軟件學(xué)院副教授，博士生導(dǎo)師,，畢業(yè)于日本北陸先端科學(xué)技術(shù)大學(xué)院大學(xué),。中國計算機學(xué)會高級會員，形式化方法專業(yè)委員會常務(wù)委員,。主要研究方向為形式化驗證,、程序語言理論、智能系統(tǒng)驗證與安全,。主持國家自然科學(xué)基金四項,、自然科學(xué)基金重點子課題一項。已經(jīng)在主流會議和知名期刊發(fā)表論文超百篇,，包括 OPPSLA,、ASE、FSE,、ICSE,、CSCW等頂級會議以及TSE、TSC、TDSC ,、TSMCA,、TDSC、 TECS等頂級期刊,。獲ICSE 2020最佳論文獎,。