通信地址： 北京市中关村南四街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 ） 同步数据流模型最佳化研究, 参与, 国家级