软件所形式化吴志林研究员

报告生成时间：2026年8月20日
个人主页：吴志林
所属团队：中国科学院软件研究所 / 基础软件与系统重点实验室 / 计算机科学国家重点实验室

一、学者基本信息

项目	信息
姓名	吴志林（男）
现任职务	中国科学院软件研究所研究员（2019年10月起）、博士生导师；基础软件与系统重点实验室常务副主任；基础软件验证研究室（VerSys）负责人
教育背景	1998—2002年中南大学应用数学与软件系学士；2002—2007年中国科学院软件研究所计算机科学国家重点实验室硕博连读博士（专业：计算机软件与理论）
研究领域	计算机软硬件基础设施的形式化验证（芯片设计验证、操作系统验证、编译器验证）、约束求解（字符串约束、分离逻辑约束）、程序验证（C/Rust程序内存安全性验证）、定理证明自动化、自动机理论
招生专业与方向	081202 计算机软件与理论；计算机软硬件基础设施形式化验证、约束求解、程序验证
学术兼职	CCF形式化方法专业委员会秘书长（2024—2028）；国际会议ATVA 2022程序委员会共同主席；CAV、CONCUR、ATVA等国际会议程序委员会委员
教授课程	离散数学、离散数学（习题课）、计算机算法设计与分析、自动机理论及其应用
联系方式	wuzl@ios.ac.cn；北京市海淀区中关村南四街4号中科院软件所基础软件与系统重点实验室（100190）

吴志林是国内形式化方法领域具有代表性的青年学者。其学术网络具有"理论—工具—产业"三位一体的特征：他一方面延续了中科院软件所从唐稚松、董蕴美、周巢尘、林惠民四位院士开创的形式化方法研究传统，另一方面通过博士后阶段的法国合作经历建立起中法学术桥梁，近年则将形式化验证技术向RISC-V处理器、操作系统、编译器等软硬件基础设施方向深度推进，实现了从理论算法到工程专利的转化。

二、教育背景与职业履历

吴志林1998年进入中南大学应用数学与软件系攻读本科，2002年获学士学位后进入中国科学院软件研究所计算机科学国家重点实验室硕博连读，2007年获工学博士学位。其博士阶段即处于中国形式化方法研究的核心学术环境之中——该实验室自上世纪80年代起即从事相关研究，先后涌现唐稚松、董蕴美、周巢尘、林惠民四位中科院院士。吴志林从读博起即受实验室老一辈科学家熏陶，立志从事形式化方法研究。

2007年博士毕业后，其职业轨迹呈现"国内—法国—国内"交替拓展的特点。2007年7月至2009年7月在中国科学院自动化研究所中法信息、自动化与应用数学联合实验室从事博士后研究，形成与自动化所在信息与自动控制交叉方向的连接。2009年9月至2010年7月在法国波尔多大学LaBRI实验室从事博士后研究，由此建立与法国理论计算机科学界的深度连接。2010年8月正式回归中科院软件所任助理研究员，2012年7月晋升副研究员。2014年6月至2015年6月以国家留学基金委公派访问学者身份赴法国巴黎第七大学LIAFA（后并入IRIF）实验室开展访问研究，进一步深化中法合作。

2012年至2019年担任副研究员期间，其在存储自动机可判定扩展（LICS 2017）和字符串约束求解等方向取得突破性成果。2019年10月晋升研究员。此后，其研究重心逐步由纯理论算法向软硬件基础设施形式化验证延伸，并深度参与国家级项目——主持国家重点研发计划课题、中科院先导A项目课题、"十三五"全军共用信息系统装备预先研究项目等。

三、学生培养情况

吴志林作为中国科学院大学博士生导师，长期招收计算机软件与理论专业的硕士与博士研究生。其基础软件验证研究室（VerSys）主页显示，研究室目前开放多个岗位，包括研究员、副研究员、博士后、工程师和实习生（处理器验证/操作系统验证方向），并已发布2026年推免生招收启事。

从公开可检索的论文署名与软件所科研进展来看，其指导或合作培养的学生及团队成员包括申世东、刘锦宇、冯维直、宋富等，这些人员在RISC-V处理器设计验证、SAT/SMT求解、程序验证等方向均有署名成果。例如2025年软件所发布的BMCFuzz混合验证方法论文，作者序列为申世东、刘锦宇、冯维直、宋富、吴志林，展示了其团队在RISC-V指令一致性验证方向的合作产出。此外，研究室主页显示2026年4月有三名毕业生顺利毕业，论文被ISSTA'26、JSA'26、FM'26、TDSC'26等国际会议和期刊录用，说明其培养体系在国际高水平学术产出方面具有持续能力。

需要指出的是，吴志林的论文作者排序遵循姓名字母序惯例，因此仅凭作者排列顺序不能直接判断指导关系。从培养主题来看，其研究生训练覆盖芯片设计形式化验证、操作系统验证、编译器验证、约束求解、程序内存安全验证等方向，形成了从理论算法到工程验证的复合型培养路径。

四、学术合作网络

4.1 内部：软件所与中科院体系

吴志林在软件所内部的合作关系首先体现为基础软件与系统重点实验室的组织协同，并嵌入CCF形式化方法专业委员会的学术共同体之中。

周巢尘、林惠民：两位中科院院士是软件所形式化方法研究的开创者和学术传统的奠基人。吴志林从读博起即受其学术传统熏陶，属于该学术谱系的继承者与拓展者。周巢尘与詹乃军曾合著《形式语义学导论》（Introduction to Formal Semantics, Academic Press, 2017），构成了该谱系的理论传承脉络。
詹乃军：现为北京大学计算机学院博雅特聘教授（2024年起，兼任）、中科院软件所研究员，国家杰出青年科学基金获得者，CCF形式化方法专委会主任。曾任中科院特聘研究员、计算机科学国家重点实验室执行主任。吴志林担任专委会秘书长，与詹乃军形成"主任—秘书长"的正式组织协同关系，共同推动全国形式化方法学术共同体的建设，包括CCF走进高校系列活动、中国软件大会等形式化方法方向的学术交流。
张立军：中科院软件所研究员，与吴志林共同领导"可信智能系统团队"，从事可信人工智能、软件验证、硬件设计验证等方面的基础理论、算法与工具研究。该团队在2021年第三届OPPO安全AI挑战赛中获得季军，成员包括李仞珏博士生、杨鹏飞助理研究员等，展示了"形式化方法+人工智能安全"交叉方向的团队协作能力。
蔡少伟：中科院软件所研究员，CCF形式化方法专委会委员。蔡少伟团队在SAT、SMT、MaxSAT等国际比赛中多次取得佳绩，研发了电路SAT求解器X-SAT。吴志林与蔡少伟、马菲菲曾合著CCF术语快线"可满足性模理论"条目，体现了软件所在约束求解方向内部的学术协同。此外，詹乃军、陈玉芳、吴志林、夏璧灿在字符串约束求解方向亦有合作论文（Acta Informatica, 2024），进一步印证了内部跨团队协作网络。
宋富：中科院软件所研究员，与吴志林在密码电路形式化验证、RISC-V处理器验证等方向有紧密合作。2024年FM会议论文《Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks》和2025年BMCFuzz工作均显示了两人在芯片设计验证方向的协作。

4.2 跨机构：高校与产业协同

吴志林的跨机构网络主要通过CCF形式化方法专委会的学术活动、国家级项目和产学研合作形成。

在学术活动层面，作为专委会秘书长，吴志林频繁参与CCF走进高校系列活动，先后走访烟台大学、内蒙古大学、首都师范大学、同济大学等高校。在烟台大学活动中，与詹乃军（北京大学）、顾斌（北京控制工程研究所）、陈钢（南京航空航天大学）、杨逸（北京控制工程研究所）等专家共同做学术报告，形成了跨机构的学术交流网络。在内蒙古大学活动中，与宋富（中科院软件所）、李钦（华东师范大学）、袁胜浩（浙江大学区块链与数据安全全国重点实验室）等同台报告，扩展了与区块链安全、大模型可信等交叉方向的连接。

在产业技术协同层面，吴志林与芯片设计企业、EDA工具厂商以及操作系统和编译器开发团队建立了合作关系。其专利成果中"RISC-V处理器Chisel设计指令集一致性的形式验证方法及装置"（专利号CN116701085A，第3作者）和多项Chisel断言语言扩展及形式化验证方法专利（CN115496017系列，第4作者），显示了在硬件敏捷设计验证方向的产业化布局。此外，软件所与香山RISC-V处理器团队存在形式化验证合作——在RISC-V中国峰会上，软件所同学曾带来《香山缓存系统的形式化验证》专题报告，而吴志林团队在BMCFuzz、RISC-V ISA一致性模型检测等方向的成果（JSA'26录用），正是这一合作的理论工具支撑。

在跨学科协作层面，吴志林与密码学、区块链、人工智能安全等方向的学者通过CCF专委和学术会议形成连接。其合作论文涵盖密码电路故障注入攻击的形式化验证（FM 2024）、安卓多任务机制形式化与静态分析（Formal Aspects of Computing, 2025）、智能合约语言翻译（专利CN116149671B）等，体现了形式化方法向安全攸关应用领域的渗透。

4.3 国际：中法合作桥梁

吴志林的国际学术网络以中法合作为最显著特征。其两次法国学术经历构成两条互补的国际连接线。

第一条线是法国波尔多大学LaBRI实验室（2009—2010年博士后），LaBRI是法国理论计算机科学的重要研究机构，在自动机理论、逻辑与算法等方向有深厚积累。吴志林在此期间的训练与其后续在存储自动机、字符串约束求解等方向的成果直接相关。

第二条线是法国巴黎第七大学LIAFA/IRIF实验室（2014—2015年国家留学基金委公派访问学者），LIAFA（后并入IRIF）是法国在自动机、形式语言与验证领域的旗舰实验室。该访问经历进一步深化了其在自动机理论与程序验证方向的国际视野。

在国际学术服务方面，吴志林担任国际会议ATVA 2022程序委员会共同主席，并长期担任CAV（计算机辅助验证旗舰会议）、CONCUR（并发理论）、ATVA（自动技术验证与分析）等国际会议程序委员会委员，这些职务使其嵌入国际形式化方法学术共同体，并与全球同行形成持续的审稿与学术组织协作网络。其参与研制的字符串约束求解器OSTRICH获得2023年度国际SMT求解器竞赛字符串理论第一名，是该国际连接在工具产出层面的具体体现。

五、业界合作关系深度分析

吴志林的业界合作网络具有"理论验证工具化、验证工具产业化"的鲜明特征，可从四个维度分析。

第一，芯片设计验证的产业化布局最为突出。形式化验证在芯片设计流程中占据近一半的成本和时间，Cadence、Synopsys、Siemens三大EDA厂商均包含成熟的芯片设计形式验证工具。吴志林团队在RISC-V处理器Chisel设计指令集一致性验证、Chisel断言语言类SVA扩展及形式化验证等方向持有多项发明专利，并与香山开源RISC-V处理器团队建立合作。2025年发布的BMCFuzz混合验证方法将限界模型检测（BMC）与覆盖率引导模糊测试（CGF）双向融合，直接面向现代处理器多级缓存、乱序执行等复杂架构的验证难题，具有明确的工程落地指向。

第二，操作系统与编译器验证连接国产基础软件生态。吴志林研究室的三大核心方向之一即操作系统验证和编译器验证。CCF形式化方法专委会主任詹乃军在国产多核实时操作系统微内核形式验证方面的实践（2.5万行系统源码验证、45万行Coq代码、通过CC EAL5+安全认证）为该方向提供了产业标杆，而吴志林作为秘书长在专委层面的组织协调，使其能够连接国内操作系统验证的主要力量。

第三，C/Rust程序内存安全验证面向系统编程语言安全需求。Rust语言因其内存安全特性在系统编程领域快速崛起，但Rust程序的安全验证仍面临分离逻辑约束求解等理论挑战。吴志林在分离逻辑、字符串约束求解方向的长期积累，使其团队具备将理论工具应用于Rust安全验证的能力，这一方向亦在研究室招生信息中明确列出。

第四，大语言模型赋能形式化验证。2026年6月，吴志林在烟台大学CCF活动中报告《大语言模型赋能形式化验证：机遇与挑战》，围绕大模型辅助约束求解、模型检测、程序终止性分析等方向展示实验室最新进展。这表明其研究已从传统形式化方法向AI驱动的验证范式拓展，可能形成与AI企业、大模型团队的新的合作空间。

六、重要奖项与学术兼职

吴志林于2020年9月29日获"CCF-IEEE CS青年科学家奖"，该奖项由CCF与IEEE计算机学会联合颁发，以表彰其在自动机理论和程序验证方面的突出贡献。其两项代表性成果分别为：存储自动机的含有算术操作的可判定扩展（LICS 2017），通过控制流与数据流相分离的思想提出RA_Q模型，保持可判定性同时允许线性算术操作，可直接应用于MapReduce平台Reducer程序的形式化建模和自动验证；字符串约束求解理论与算法的突破，最终催生OSTRICH求解器在2023年国际SMT竞赛字符串理论中获得第一名。

在学术兼职方面，吴志林担任CCF形式化方法专业委员会秘书长（2024—2028），此前曾任该专委副秘书长。作为秘书长，他主持了2024 CCF中国软件大会颁奖环节，并组织了多场CCF走进高校活动。在国际层面，他担任ATVA 2022程序委员会共同主席，以及CAV、CONCUR、ATVA等顶级会议的程序委员会委员。此外，他与蔡少伟、马菲菲合著的CCF术语快线"可满足性模理论"条目，为国内SMT领域的术语规范和知识传播做出了贡献。

在专利方面，其团队持有的发明专利覆盖RISC-V处理器Chisel设计指令集一致性形式验证（CN116701085A）、Chisel断言语言类SVA扩展及形式化验证（CN115496017A/B）、智能合约语言翻译方法与装置（CN116149671B）等方向，构成了从芯片验证到区块链智能合约的应用专利矩阵。

七、Connection圈层总结

吴志林的关系网络可概括为五个相互嵌套的圈层。

核心团队圈：以中科院软件所基础软件与系统重点实验室基础软件验证研究室（VerSys）为组织基础，吴志林作为负责人，联合张立军（可信智能系统团队共同领导）、宋富（密码电路与处理器验证合作者）等软件所内部研究员，形成覆盖芯片验证、操作系统验证、程序验证、约束求解和可信AI的内部协作核心。该圈层的产出体现为OSTRICH求解器、BMCFuzz方法、VeriSAT FPGA求解器等工具和多项专利。
学术传承圈：以软件所计算机科学国家重点实验室为根基，上承唐稚松、董蕴美、周巢尘、林惠民四位院士开创的形式化方法学术传统，旁接詹乃军（现北京大学）所代表的实时/混成系统与程序验证谱系。詹乃军与周巢尘合著的《形式语义学导论》是该谱系传承的书面标志。
全国学术共同体圈：通过CCF形式化方法专委会秘书长身份，吴志林连接詹乃军（主任）、蔡少伟（委员）、陈钢（南京航空航天大学）、顾斌（北京控制工程研究所）、宋富（软件所）、李钦（华东师范大学）、袁胜浩（浙江大学）等全国形式化方法领域骨干学者，并通过CCF走进高校活动覆盖烟台大学、内蒙古大学、首都师范大学、同济大学等高校，形成学术传播与人才培养的全国网络。
中法国际合作圈：以法国波尔多大学LaBRI实验室和巴黎第七大学LIAFA/IRIF实验室为两个锚点，通过两次法国学术经历建立的中法理论计算机科学连接，延伸至ATVA 2022程序委员会共同主席和CAV、CONCUR等国际会议程序委员会委员身份，形成嵌入国际形式化方法学术共同体的持续通道。
产业转化圈：以RISC-V处理器验证（含香山处理器合作、Chisel设计验证专利）、操作系统与编译器验证、C/Rust内存安全验证、智能合约验证为应用出口，连接芯片设计企业、EDA工具生态、国产操作系统团队和区块链安全应用方，形成"理论算法—验证工具—工程专利—产业落地"的完整转化链条。

总体而言，吴志林是形式化方法领域典型的"理论—工具—产业"复合型学者。其Connection网络的核心竞争力，在于将软件所形式化方法学术传统、中法国际合作通道、CCF专委全国学术共同体组织职能，以及RISC-V和基础软件验证的产业需求，通过基础软件验证研究室这一平台有机整合，形成了从可判定性理论突破到工程专利产出的完整价值链。

主要公开资料： 国科大吴志林主页；基础软件验证研究室主页；百度百科吴志林；CCF青年科学家奖报道；同济大学学术报告介绍；软件所SAT与RISC-V验证进展；CCF形式化方法专委走进烟台大学；詹乃军北京大学主页；软件所可信智能团队OPPO安全AI挑战赛。

软件所形式化 吴志林 研究员