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

研究领域

程序的自动分析与验证,计算逻辑,形式语言与自动机理论

招生信息

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

招生专业
081202-计算机软件与理论
085400-电子信息
招生方向
对以下类型程序的自动分析与验证:操作字符串的程序、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-25-2020-12-30,中国计算机学会形式化方法专业组成员,

教授课程

离散数学
自动机理论及其应用
自动机理论及其应用
这是一门针对中科院软件所博士生的专业基础课程。

课程的目标是对自动机理论作一个相对全面的介绍。同时关注自动机理论在形式验证与数据库理论方面的应用。

如果想了解课程的更多信息,可以访问 http://lcs.ios.ac.cn/~wuzl/teaching.html

专利与奖励

   
奖励信息
(1) CCF-IEEE青年科学家奖, 其他, 2020

出版信息

   
发表论文(除极特殊情况外,论文作者均以姓名字母序排列)
[1] Chen, Taolue, Lamas, Alejandro Flores, Hague, Matthew, Han, Zhilei, 胡登杭, Kan, Shuanglong, Lin, Anthony Widjaja, Ruemmer, Philipp, Wu, Zhilin. Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. POPL 2022null. 2022, [2] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, 胡登杭, Wei-Lun Tsai, 吴志林, Di-De Yen. Solving Not-Substring Constraint withFlat Abstraction. APLAS 2021null. 2021, [3] Nicolas Peltier, Viorica SofronieStokkermans, Matthew Hague, Anthony W Lin, Philipp Rmmer, Zhilin Wu. Monadic Decomposition in Integer Linear Arithmetic. Automated Reasoning. 2020, 12166: 122-140, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324128/.
[4] Chen Taolue, Hague Matthew, He Jinlong, Hu Denghang, Lin Anthony Widjaja, Rummer Philipp, Wu Zhilin. A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. 2020, http://arxiv.org/abs/2007.06913.
[5] 吴志林. Computing Linear Arithmetic Representation of Reachability Relation of One-counter Automata. Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA 2020). 2020, [6] He, Jinlong, Chen, Taolue, Wang, Ping, Wu, Zhilin, Yan, Jun, Lin, AW. Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2019null. 2019, 11893: 291-312, [7] Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rmmer, Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proceedings of the ACM on Programming Languages. 2019, 3: [8] Gao, Chong, Chen, Taolue, Wu, Zhilin, Catania, B, Kralovic, R, Nawrocki, J, Pighizzini, G. Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. THEORY AND PRACTICE OF COMPUTER SCIENCE, SOFSEM 2019null. 2019, 11376: 206-220, [9] Chen Taolue, He Jinlong, Song Fu, Wang Guozhen, Wu Zhilin, Yan Jun, Chockler H, Weissenbacher G. Android Stack Machine. COMPUTER AIDED VERIFICATION, CAV 2018, PT IInull. 2018, 10982: 487-504, [10] Chen, YuFang, Lengal, Ondrej, Tan, Tony, Wu, Zhilin, IEEE. Register automata with linear arithmetic. 2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)null. 2017, [11] Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, Zhilin Wu. What is decidable about string constraints with the ReplaceAll function. Proceedings of the ACM on Programming Languages. 2017, 2: [12] Chen Taolue, Song Fu, Wu Zhilin, Bowen JP, Liu Z, Zhang Z. Formal Reasoning on Infinite Data Values: An Ongoing Quest. ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016)null. 2017, 10215: 195-257, [13] 吴志林. Tractability of separation logic with inductive definitions: Beyond lists. International Conference on Concurrency Theory (CONCUR). 2017, [14] 吴志林. The Complexity of SORE-definability Problem. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). 2017, [15] Xu Zhaowei, Chen Taolue, Wu Zhilin, DeMoura L. Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. AUTOMATED DEDUCTION - CADE 26null. 2017, 10395: 509-527, [16] 吴志林. Verifying pushdown multi-agent systems against strategy logics. International Joint Conference on Artificial Intelligence (IJCAI 2016). 2016, [17] Song, Fu, Wu, Zhilin. On temporal logics with data variable quantifications: Decidability and complexity. INFORMATION AND COMPUTATION[J]. 2016, 251: 104-139, http://dx.doi.org/10.1016/j.ic.2016.08.002.
[18] Chen Taolue, Song Fu, Wu Zhilin, AAAI. Global Model Checking on Pushdown Multi-Agent Systems. THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCEnull. 2016, 2459-2465, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000485474202070.
[19] Wu Zhilin, Franzle M, Kapur D, Zhan N. Semipositivity in Separation Logic with Two Variables. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONSnull. 2016, 9984: 179-196, [20] Chen YuFang, Song Lei, Wu Zhilin, Chaudhuri S, Farzan A. The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT IInull. 2016, 9780: 91-111, [21] Gu Xincai, Chen Taolue, Wu Zhilin, Olivetti N, Tiwari A. A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. AUTOMATED REASONING (IJCAR 2016)null. 2016, 9706: 532-549, [22] 吴志林. On the Satisfiability of Indexed Linear Temporal Logics. 26th International Conference on Concurrency Theory (CONCUR 2015). 2015, [23] Enea Constantin, Sighireanu Mihaela, Wu Zhilin, Finkbeiner B, Pu G, Zhang L. On Automated Lemma Generation for Separation Logic with Inductive Definitions. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015null. 2015, 9364: 80-96, [24] 吴志林. On effective construction of the greatest solution of language inequality $XA \subseteq BX$. Theoretical Computer Science. 2014, [25] 吴志林. Extending Temporal Logics with Data Variable Quantifications. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). 2014, [26] 吴志林. Recursive queries on trees and data trees. The 16th International Conference on Database Theory (ICDT 2013). 2013, [27] Zhilin Wu. A Decidable Extension of Data Automata. Electronic Proceedings in Theoretical Computer Science[J]. 2011, 54: 116-130, https://doaj.org/article/2a327cc7c5954873ba11ea441dcc3f5f.
[28] Wu, Zhilin, Grumbach, Stephane. Feasibility of motion planning on acyclic and strongly connected directed graphs. DISCRETE APPLIED MATHEMATICS[J]. 2010, 158(9): 1017-1028, http://dx.doi.org/10.1016/j.dam.2010.02.001.
[29] Grumbach Stephane, Wu Zhilin, Paul C, Habib M. Logical Locality Entails Frugal Distributed Computation over Graphs. GRAPH-THEORETIC CONCEPTS IN COMPUTER SCIENCEnull. 2010, 5911: 154-165, [30] 吴志林. 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, [31] Wu Zhilin, Grumbach Stephane, Chen J, Cooper SB. Feasibility of Motion Planning on Directed Graphs. THEORY AND APPLICATIONS OF MODELS OF COMPUTATIONnull. 2009, 5532: 430-439, [32] Wu, Zhilin. A note on the characterization of TLEF. INFORMATION PROCESSING LETTERS[J]. 2007, 102(2-3): 48-54, http://www.corc.org.cn/handle/1471x/2380343.
[33] Wu Zhilin. On the expressive power of qltl. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)null. 2007, 467-481, http://124.16.136.157/handle/311060/11130.
[34] Wu Zhilin. Quasi-star-free Languages on Infinite Words. ACTA CYBERNETICA[J]. 2005, 17(1): 75-93, [35] Zhilin Wu. Commutative Data Automata. CEUR. http://oa.las.ac.cn/oainone/service/browseall/read1?ptype=CA&workid=CA201702140000157CD.

科研活动

   
科研项目
( 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
( 6 ) 内生安全应用构造技术, 主持, 国家级, 2019-04--2020-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-计算机软件与理论  

胡登杭  硕士研究生  081202-计算机软件与理论  

傅宣登  硕士研究生  081200-计算机科学与技术  

朱雨田  硕士研究生  081202-计算机软件与理论