基本信息
吴志林男 研究员 硕导中国科学院软件研究所
电子邮件： wuzl@ios.ac.cn
通信地址： 北京市中关村南四街4号中科院软件所计算机科学国家重点实验室
邮政编码： 100190

部门/实验室：计算机科学国家重点实验室
研究领域
程序的自动分析与验证，计算逻辑，形式语言与自动机理论


招生信息



如果你是一名对以下方向感兴趣的高年级本科生，欢迎联系我（包括实习、硕士研究生保送推荐与考试）。
1、程序的自动分析与验证（比如对大数据流处理程序、Android程序、Javascript程序等的分析与验证），
2、计算逻辑（比如时序逻辑、分离逻辑、字符串约束等），
3、形式语言与自动机理论（比如正规表达式、有限自动机、下推自动机等）。
更多信息请访问个人主页：http://lcs.ios.ac.cn/~wuzl





招生专业081202-计算机软件与理论
085211-计算机技术

招生方向对以下类型程序的自动分析与验证：大数据流处理程序、操作字符串的程序、Android程序、操作操作动态数据结构的程序


教育背景2002-09--2007-06中国科学院软件研究所计算机科学国家重点实验室硕博连读、博士
1998-09--2002-06中南大学应用数学与软件系本科、学士

学历
学位工学博士（专业：计算机软件与理论）

工作经历
工作简历2019-10~现在,中国科学院软件研究所计算机科学国家重点实验室,研究员
2014-06~2015-06,法国巴黎第七大学LIAFA实验室,国家留学基金委公派访问
2012-07~2019-09,中国科学院软件研究所计算机科学国家重点实验室,副研究员
2010-08~2012-07,中国科学院软件研究所计算机科学国家重点实验室,助理研究员
2009-09~2010-07,法国波尔多大学LaBRI实验室,博士后
2007-07~2009-07,中科院自动化所中法信息、自动化与应用数学联合实验室,博士后

社会兼职2016-01-27-2019-12-31,中国计算机学会形式化方法专业组成员,


教授课程自动机理论及其应用

自动机理论及其应用这是一门针对中科院软件所博士生的专业基础课程。
课程的目标是对自动机理论作一个相对全面的介绍。同时关注自动机理论在形式验证与数据库理论方面的应用。
如果想了解课程的更多信息，可以访问 http://lcs.ios.ac.cn/~wuzl/teaching.html

专利与奖励
奖励信息
专利成果

出版信息
发表论文（除极特殊情况外，论文作者均以姓名字母序排列）（1）Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps,17th Asian Symposium on Programming Languages and Systems (APLAS 2019),2019-12,第4作者
（2）Decision procedures for path feasibility of string-manipulating programs with complex operations,46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019),2019,第5作者
（3）Separation logic with linearly compositional inductive predicates and set data constraints,45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2019),2019,第3作者
（4）Android Stack Machine,30th International Conference on Computer Aided Verification (CAV 2018),2018,第5作者
（5）What is decidable about string constraints with the replaceAll function,45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018),2018,第5作者
（6）The Complexity of SORE-definability Problem,42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017),2017,第2作者
（7）Tractability of separation logic with inductive definitions: Beyond lists,28th International Conference on Concurrency Theory (CONCUR 2017),2017,第3作者
（8）Register automata with linear arithmetic,Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017),2017,通讯作者
（9）Satisfiability of compositional separation logic with tree predicates and data constraints,The 26th International Conference on Automated Deduction (CADE 2017),2017,通讯作者
（10）Semipositivity In Separation Logic With Two Variables,Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2016),2016,第1作者
（11）On temporal logics with data variable quantifications: decidability and complexity,Information and Computation,2016,通讯作者
（12）The commutativity problem of the MapReduce framework: A transducer-based approach,International Conference on Computer Aided Verification (CAV 2016),2016,通讯作者
（13）Global model checking of pushdown multi-agent systems,AAAI Conference on Artificial Intelligence (AAAI 2016),2016,通讯作者
（14）Verifying pushdown multi-agent systems against strategy logics,International Joint Conference on Artificial Intelligence (IJCAI 2016),2016,通讯作者
（15）Formal Reasoning on Infinite Data Values: An Ongoing Quest,Engineering Trustworthy Software Systems - Second International School (SETSS 2016),2016,通讯作者
（16）A complete decision procedure for linearly compositional separation logic with data constraints,International Joint Conference on Automated Reasoning (IJCAR 2016),2016,通讯作者
（17）On Automated Lemma Generation for Separation Logic with Inductive Definitions,13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015),2015,通讯作者
（18）On the Satisfiability of Indexed Linear Temporal Logics,26th International Conference on Concurrency Theory (CONCUR 2015),2015,通讯作者
（19）On effective construction of the greatest solution of language inequality $XA \subseteq BX$,Theoretical Computer Science,2014,通讯作者
（20）Extending Temporal Logics with Data Variable Quantifications,34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014),2014,通讯作者
（21）Recursive queries on trees and data trees,The 16th International Conference on Database Theory (ICDT 2013),2013,通讯作者
（22）Commutative Data Automata,The 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012),2012,通讯作者
（23）A Decidable Extension of Data Automata,The 2nd International Symposium on Games,Automata, Logics and Formal Verification (GandALF 2011),2011,通讯作者
（24）Feasibility of Motion Planning on Acyclic and Strongly-connected Directed Graphs,Discrete Applied Mathematics, volume 158(9), pages 1017-1028,2010,通讯作者
（25）Logical Locality Entails Frugal Distributed Computation Over Graphs,The 35th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2009),2010,通讯作者
（26）Verifying Active Documents with Positive Data Tree Pattern Rewriting,Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010),2010,第3作者
（27）Feasibility of Motion Planning on Directed Graphs,The 6th Annual Conference on Theory and Applications of Models of Computation (TAMC 2009),2009,第1作者
（28）On the Expressive Power of QLTL,The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007),2007,第1作者
（29）A Note on the Characterization of TL[EF],Information Processing Letters, volume 102, pages 48-54,2007,第1作者
（30）Quasi-star-free Languages on Infinite Words,Acta Cybernetica, volume 17(1), pages 75-93,2005,第1作者

发表著作

科研活动
科研项目（ 1 ） 无穷字母表上的形式模型：逻辑与自动机, 主持,国家级,2012-01--2014-12
（ 2 ） 符号模型与隐式模型检测技术, 参与,国家级,2013-01--2016-12
（ 3 ） 动态数据结构的形状性质与数据约束：基于分离逻辑的自动分析与验证, 主持,国家级,2015-01--2018-12
（ 4 ） 同步数据流模型优化研究, 参与,国家级,2016-01--2019-12
（ 5 ） 分布式流处理程序的分析与验证, 主持,国家级,2019-01--2022-12

参与会议

合作情况



与国内外同行有广泛合作。国外合作包括：
-- 法国：巴黎七大LIAFA实验室的Ahmed Bouajjani教授(https://www.irif.fr/~abou/)、Mihaela Sighireanu博士(https://www.irif.fr/~sighirea/)
-- 英国：Birkbeck,University of London的陈韬略博士(http://www.dcs.bbk.ac.uk/~taolue/)，Royal Holloway, University of London的Matthew Hague博士（http://www.cs.rhul.ac.uk/home/hague/）
--德国：TU Kaiserslautern的Anthony W. Lin博士（https://anthonywlin.github.io/）
-- 瑞典：Uppsala University大学的Philipp Ruemmer博士（http://www.philipp.ruemmer.org/）
-- 捷克：Brno University of Technology的Ondrej Lengal博士（https://www.fit.vutbr.cz/~lengal/）
-- 台湾：中央研究院资讯研究所的陈郁方博士（https://www.iis.sinica.edu.tw/pages/yfc/）、National Taiwan University的Tony Tan博士(https://www.csie.ntu.edu.tw/~tonytan/)






项目协作单位

指导学生已指导学生
古新才硕士研究生081202-计算机软件与理论
陈艳硕士研究生081202-计算机软件与理论
高冲硕士研究生081202-计算机软件与理论
现指导学生
苏婉昀硕士研究生081202-计算机软件与理论