基本信息

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

研究领域

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

招生信息

如果你是一名对以下方向感兴趣的高年级本科生,欢迎联系我(包括实习、硕士研究生保送推荐与考试)。
1、程序的形式化分析与验证(比如对大数据平台Hadoop、SPARK等上的程序、Android平台上的程序、Javascript程序的分析与验证),
2、计算逻辑(比如时序逻辑、分离逻辑等),
3、形式语言与自动机理论(比如正规表达式、有限自动机、下推自动机等),
4、数据库查询语言相关的理论研究(比如XPath、DATALOG、SPARQL等)。

更多信息请访问个人主页:http://lcs.ios.ac.cn/~wuzl

招生专业
081202-计算机软件与理论
085211-计算机技术
招生方向
大数据平台上的程序的自动分析与验证,对操作动态数据结构的程序的自动分析与验证,云计算平台和智能手机的安全与隐私问题
图数据库(比如RDF数据)的查询语言理论研究

教育背景

2002-09--2007-06   中国科学院软件研究所计算机科学国家重点实验室   硕博连读、博士
1998-09--2002-06   中南大学应用数学与软件系   本科、学士
学历
   
学位
工学博士(专业:计算机软件与理论)

工作经历

   
工作简历
2014-06~2015-06,法国巴黎第七大学LIAFA实验室, 国家留学基金委公派访问学者
2012-07~现在, 中科院软件所计算机科学国家重点实验室, 副研究员
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) The Complexity of SORE-definability Problem, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), 2017, 第 2 作者
(2) Register automata with linear arithmetic, Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 2017, 通讯作者
(3) Satisfiability of compositional separation logic with tree predicates and data constraints, The 26th International Conference on Automated Deduction (CADE 2017), 2017, 通讯作者
(4) Semipositivity In Separation Logic With Two Variables, Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2016), 2016, 第 1 作者
(5) On temporal logics with data variable quantifications: decidability and complexity, Information and Computation, 2016, 通讯作者
(6) The commutativity problem of the MapReduce framework: A transducer-based approach, International Conference on Computer Aided Verification (CAV 2016), 2016, 通讯作者
(7) Global model checking of pushdown multi-agent systems, AAAI Conference on Artificial Intelligence (AAAI 2016), 2016, 通讯作者
(8) Verifying pushdown multi-agent systems against strategy logics, International Joint Conference on Artificial Intelligence (IJCAI 2016), 2016, 通讯作者
(9) Formal Reasoning on Infinite Data Values: An Ongoing Quest, Engineering Trustworthy Software Systems - Second International School (SETSS 2016), 2016, 通讯作者
(10) A complete decision procedure for linearly compositional separation logic with data constraints, International Joint Conference on Automated Reasoning (IJCAR 2016), 2016, 通讯作者
(11) On Automated Lemma Generation for Separation Logic with Inductive Definitions, 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), 2015, 通讯作者
(12) On the Satisfiability of Indexed Linear Temporal Logics, 26th International Conference on Concurrency Theory (CONCUR 2015), 2015, 通讯作者
(13) On effective construction of the greatest solution of language inequality $XA \subseteq BX$, Theoretical Computer Science, 2014, 通讯作者
(14) Extending Temporal Logics with Data Variable Quantifications, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), 2014, 通讯作者
(15) Recursive queries on trees and data trees, The 16th International Conference on Database Theory (ICDT 2013), 2013, 通讯作者
(16) Commutative Data Automata, The 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012), 2012, 通讯作者
(17) A Decidable Extension of Data Automata, The 2nd International Symposium on Games,Automata, Logics and Formal Verification (GandALF 2011), 2011, 通讯作者
(18) Feasibility of Motion Planning on Acyclic and Strongly-connected Directed Graphs, Discrete Applied Mathematics, volume 158(9), pages 1017-1028, 2010, 通讯作者
(19) Logical Locality Entails Frugal Distributed Computation Over Graphs, The 35th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2009), 2010, 通讯作者
(20) 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 作者
(21) Feasibility of Motion Planning on Directed Graphs, The 6th Annual Conference on Theory and Applications of Models of Computation (TAMC 2009), 2009, 第 1 作者
(22) On the Expressive Power of QLTL, The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007), 2007, 第 1 作者
(23) A Note on the Characterization of TL[EF], Information Processing Letters, volume 102, pages 48-54, 2007, 第 1 作者
(24) 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
参与会议
   

合作情况

与国内外同行有广泛合作。国外合作包括:
-- 法国:巴黎七大LIAFA实验室的Ahmed Bouajjani教授、Constantin Enea博士、Mihaela Sighireanu博士等,波尔多一大LaBRI实验室的Anca Muscholl教授、CNRS研究员Gabriele Puppis等,雷恩一大IRISA实验室的CNRS研究员Blaise Genest,INRIA的links项目的CNRS研究员Pierre Bourhis

-- 英国:MiddleSex大学的陈韬略博士、Oxford大学的Anthony W. Lin博士

-- 台湾:中央研究院资讯研究所的陈郁方博士、National Taiwan University的Tony Tan博士

-- 捷克:Brno University of Technology的Ondrej Lengal博士

项目协作单位
   

指导学生

现指导学生

古新才  02  19261  

陈艳  02  19261  

高冲   02  19261