软件自动验证的追梦者——吴志林，2020年CCF-IEEE CS青年科学家奖获得者

CCF理事长梅宏教授（左一）、百度校园品牌部总监李轩涯博士（右一）为吴志林研究员颁奖

吴志林本科就读于中南大学，博士毕业于中国科学院软件研究所计算机科学国家重点实验室。博士毕业之后，先后在中国科学院自动化研究所中法联合实验室和法国波尔多第一大学LaBRI实验室从事博士后研究。2010年加入中国科学院软件研究所工作，2014-2015在法国巴黎第七大学IRIF实验室担任国家公派访问学者。

计算机科学国家重点实验室是中国形式化方法的研究中心之一，该实验室从上世纪80年代开始就从事相关研究工作，先后涌现了一批杰出的计算机科学家，包括唐稚松、董蕴美、周巢尘、林惠民四位中科院院士。吴志林从读博士开始就受到实验室老一辈科学家的熏陶，立志于从事形式化方法的研究工作。他的研究方向包括计算逻辑、自动机理论、程序验证等，在时序逻辑、分离逻辑、无穷数据域上的自动机模型、字符串约束求解、安卓多任务机制等方面取得了丰硕的成果，代表性贡献集中于存储自动机的带算术操作的可判定扩展和字符串约束求解理论与算法的突破。

如何保证软件的正确性是计算机科学的经典问题，其起源可以追溯至图灵1949年的题为”Checking A Large Routine”的论文。自动机和逻辑是软件正确性自动形式化验证的理论基础，其相关问题的判定算法是实现软件自动验证的关键，吴志林研究员在这一极富挑战性的领域中取得了两项代表性研究成果。

挑战：存储自动机(Register Automata, RA)是一个经典的自动机模型，在该模型中引入算术操作将导致不可判定性，而不含有算术操作的存储自动机无法满足实际应用中的形式化建模和自动验证需求，因此对存储自动机的含有算术操作的可判定扩展是一个非常重要但很有挑战性的问题。

成果1. 存储自动机的含有算术操作的可判定扩展(LICS 2017)

他根据控制流和数据流相分离的思想，提出了存储自动机的含有算术操作的可判定扩展（简称RA_Q）。RA_Q保持了RA良好的性质，并允许某些变量上的线性算术操作，表达能力明显增强，同时其不变量问题依旧是可判定的；对于确定化RA_Q，其交换、等价和可达问题与其不变量问题是多项式时间互归约的。MapReduce平台的Reducer程序的形式化建模和自动验证可视作是RA_Q的直接应用，而这在以前是难以准确做到的。

花絮：

•2016年3月：中国台湾中研院的陈郁方博士和中科院软件所的吴志林博士定义了存储自动机的带线性算术操作的扩展，他们对于该模型的可判定性做出了不同的判断。为此他们定下了赌约，赌注是一顿牛排，因此该问题也被称为“牛排问题”( “Steak problem”)。受牛排的诱惑，台湾大学的Tony Tan博士和捷克Brno University of Technology的Ondrej Lengal博士也加入了对该问题的探讨。

•2016年8月：四位合作者经过持续攻关，证明了存储自动机的带线性算术扩展的可判定性，“牛排问题”得到了解决，陈郁方输掉了赌约。

•2016年12月：论文撰写完成，四位作者齐聚台北，陈郁方兑现了牛排赌约。

挑战：字符串是几乎每个编程语言中都存在的数据类型，字符串约束求解是对操作字符串的程序进行自动形式化验证的基础，该问题一般来讲不可判定，目前求解器基本使用不完备的启发式算法。如何寻找表达能力强的字符串约束的可判定子集并设计完备高效的判定算法是一个很有挑战性的问题。

成果2. 字符串约束的可判定性语义条件、判定算法、及实现(POPL 2018、POPL 2019、ATVA 2020)

找到表达能力强且可判定的字符串理论具有重要价值，可直接提升JavaScript、PHP等程序的分析与验证能力。吴志林提出了字符串约束的可判定性的语义条件，找到了一个包含常见字符串操作的“特定极大意义”的可判定字符串理论；基于语义条件设计了一般性的、高效、且易扩展的判定算法；并开发了国际上目前表达能力最强且与主流求解器性能相当的字符串约束求解器OSTRICH。

花絮：

•2014年，厦门大学的陈同学在报考中科院软件所的硕士研究生时，通过滑动鼠标滚轮的方式随机选中了吴志林作为导师，而且放出了要在研究生期间发一篇“惊世骇俗”的论文的豪言。

•2016年下半年，吴志林指导陈同学在字符串约束求解方面开始展开探讨。

•2017年10月，论文被编程语言顶级会议POPL接受，陈同学的“惊世骇俗”论文豪言成真。

吴志林热心学术交流和服务，联合发起了形式化方法青年学术论坛，组织国内形式化方法领域的优秀青年学者撰写了“形式化方法的研究进展与趋势”，入选了《2017-2018中国计算机科学技术发展报告》，他还担任CONFESTA2018大会的本地组委会主席，协助组织形式化方法暑期学校，推动形式化方法在我国的普及和发展。

未来，吴志林将为实现软件正确性和安全性的自动形式化验证的梦想而继续奋斗，为推动形式化方法在中国的进一步发展而继续努力！