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


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

招生专业 计算机软件与理论



招生方向 对操作动态数据结构的程序的自动分析与验证
对软件系统中的无穷数据的的分析与推理
图数据库（比如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 中科院自动化所中法信息、自动化与应用数学联合实验室 博士后


社会兼职
教授课程 自动机理论及其应用

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

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

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

奖励信息

专利成果
出版信息

发表论文 （1） On Automated Lemma Generation for Separation Logic with Inductive Definitions，13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)，2015，第3作者
（2） On the Satisfiability of Indexed Linear Temporal Logics，26th International Conference on Concurrency Theory (CONCUR 2015)，2015，第3作者
（3） On effective construction of the greatest solution of language inequality $XA subseteq BX$，Theoretical Computer Science，2014，第2作者
（4） Extending Temporal Logics with Data Variable Quantifications，34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)，2014，第2作者
（5） Recursive queries on trees and data trees，The 16th International Conference on Database Theory (ICDT), Pages 93-104，2013，第4作者
（6） Commutative Data Automata，The 21st EACSL Annual Conferences on Computer Science Logic (CSL).Leibniz International Proceedings in Informatics (LIPIcs), volume 16, pages 528-543，2012，第1作者
（7） A Decidable Extension of Data Automata，The 2nd International Symposium on Games,Automata, Logics and Formal Verification (GandALF). EPTCS, volume 54, pages 116-130，2011，第1作者
（8） Logical Locality Entails Frugal Distributed Computation Over Graphs，The 35th International Workshop on Graph-Theoretic Concepts in Computer Science (WG), volume 5911, pages 154-165，2010，第2作者
（9） Feasibility of Motion Planning on Acyclic and Strongly-connected Directed Graphs，Discrete Applied Mathematics, volume 158(9), pages 1017-1028，2010，第1作者
（10） 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).Leibniz International Proceedings in Informatics (LIPIcs), volume 8, pages 469-480，2010，第3作者
（11） Feasibility of Motion Planning on Directed Graphs，The 6th Annual Conference on Theory and Applications of Models of Computation (TAMC). LNCS, volume 5532, pages 430-439，2009，第1作者
（12） On the Expressive Power of QLTL，The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC). LNCS, volume 4711, pages 467-481，2007，第1作者
（13） A Note on the Characterization of TL[EF]，Information Processing Letters, volume 102, pages 48-54，2007，第1作者
（14） Quasi-star-free Languages on Infinite Words，Acta Cybernetica, volume 17(1), pages 75-93，2005，第1作者


发表著作
科研活动

科研项目 （1） 动态数据结构的形状性质与数据约束：基于分离逻辑的自动分析与验证，主持，国家级，2015-01--2018-08
（2） 符号模型与隐式模型检测技术，参与，国家级，2013-01--2016-12
（3） 无穷字母表上的形式模型：逻辑与自动机，主持，国家级，2012-01--2014-12


参与会议
合作情况与国内外同行有广泛合作。国外合作包括：
-- 法国巴黎七大LIAFA实验室的Ahmed Bouajjani教授、Constantin Enea博士、Mihaela Sighireanu博士等
-- 法国ENS Cachan的LSV实验室的CNRS高级研究员Stephane Demri
-- 英国MiddleSex大学的陈韬略博士
-- 法国波尔多一大LaBRI实验室的Anca Muscholl教授、CNRS研究员Gabriele Puppis等
-- 法国雷恩一大IRISA实验室的CNRS研究员Blaise Genest
-- 法国INRIA的links项目的CNRS研究员Pierre Bourhis

项目协作单位
指导学生现指导学生

古新才 硕士研究生 081202-计算机软件与理论