吳志林(中國科學院軟體研究所副研究員)

吳志林，男，碩導，中國科學院軟體研究所副研究員，研究領域：程式的形式化分析與驗證、計算邏輯、形式語言與自動機理論、資料庫理論。

基本信息

通信地址： 北京市中關村南四街4號中科院軟體所計算機科學國家重點實驗室

教育背景

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,中科院自動化所中法信息、自動化與套用數學聯合實驗室, 博士後

出版信息

（1） Semipositivity In Separation Logic With Two Variables, Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA)

（2） On temporal logics with data variable quantifications: decidability and complexity, Information and Computation

（3） The commutativity problem of the MapReduce framework: A transducer-based approach, International Conference on Computer Aided Verification (CAV)

（4） Global model checking of pushdown multi-agent systems, AAAI Conference on Artificial Intelligence (AAAI)

（5） Verifying pushdown multi-agent systems against strategy logics, International Joint Conference on Artificial Intelligence (IJCAI)

（6） A complete decision procedure for linearly compositional separation logic with data constraints, International Joint Conference on Automated Reasoning (IJCAR)

（7） On Automated Lemma Generation for Separation Logic with Inductive Definitions, 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)

（8） On the Satisfiability of Indexed Linear Temporal Logics, 26th International Conference on Concurrency Theory (CONCUR 2015)

（9） On effective construction of the greatest solution of language inequality $XA \subseteq BX$, Theoretical Computer Science

（10） Extending Temporal Logics with Data Variable Quantifications, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

（11） Recursive queries on trees and data trees, The 16th International Conference on Database Theory (ICDT)

（12） Commutative Data Automata, The 21st EACSL Annual Conferences on Computer Science Logic (CSL)

（13） A Decidable Extension of Data Automata, The 2nd International Symposium on Games,Automata, Logics and Formal Verification (GandALF). EPTCS

（14） Feasibility of Motion Planning on Acyclic and Strongly-connected Directed Graphs, Discrete Applied Mathematics

（15） Logical Locality Entails Frugal Distributed Computation Over Graphs, The 35th International Workshop on Graph-Theoretic Concepts in Computer Science (WG)

（16） 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)

（17） Feasibility of Motion Planning on Directed Graphs, The 6th Annual Conference on Theory and Applications of Models of Computation (TAMC)

（18） On the Expressive Power of QLTL, The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC)

（19） A Note on the Characterization of TL[EF], Information Processing Letters

（20） Quasi-star-free Languages on Infinite Words, Acta Cybernetica

科研項目

（ 1 ） 無窮字母表上的形式模型：邏輯與自動機, 主持, 國家級

（ 2 ） 符號模型與隱式模型檢測技術, 參與, 國家級

（ 3 ） 動態數據結構的形狀性質與數據約束：基於分離邏輯的自動分析與驗證, 主持, 國家級

（ 4 ） 同步數據流模型最佳化研究, 參與, 國家級