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

　　報(bào)告人：李國(guó)強(qiáng)

　　時(shí)間：2025年04月10日(周四)，09：00-10：00

　　會(huì)議地點(diǎn)：31-904

　　報(bào)告摘要：

　　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.

　　報(bào)告人簡(jiǎn)介：

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