摘要：

字符串在几乎每一个编程语言（尤其是与Web相关的编程语言）中广泛存在，字符串约束求解是理论计算机科学和形式化方法比较有挑战性的一个研究方向，近年来进展迅速。本报告介绍字符串约束求解器OSTRICH相关判定算法的主要思想，并对未来工作进行展望。

简介：

吴志林，中国科学院软件研究所基础软件与系统重点实验室研究员，博士生导师，2020年“CCF-IEEE CS”青年科学家奖获得者。博士毕业于中国科学院软件研究所计算机科学国家重点实验室，先后在中国科学院自动化研究所中法计算机科学、自动化与应用数学联合实验室和法国波尔多第一大学LaBRI实验室从事博士后研究。2014-2015在法国巴黎第七大学IRIF实验室担任国家留学基金委公派访问学者。长期从事计算机软硬件系统形式化验证、计算逻辑、自动机理论等相关研究，在知名国际会议和期刊上发表论文40余篇，包括LICS、POPL、CAV、DAC、Information and Computation、DAC、IJCAR、CADE、CONCUR等。先后主持多项国家级项目，包括国家重点研发计划课题、中科院先导A项目课题、“十三五”全军共用信息系统装备预先研究项目等。中国计算机学会形式化方法专业委员会秘书长，国际会议ATVA 2022、TASE 2025程序委员会共同主席，CAV、CONCUR、ATVA等国际会议的程序委员会委员。