计算机软硬件基础设施的形式化验证、定理证明自动化、程序验证、自动机理论

更多信息参见基础软件与系统重点实验室（中国科学院）基础软件验证研究室主页（https://versys.ios.ac.cn/）

如果你是一名对以下方向感兴趣的高年级本科生，欢迎联系我（包括实习、硕士研究生保送推荐与考试）。
1、计算机软硬件基础设施的形式化验证（芯片设计验证、操作系统验证、编译器验证），
2、定理证明自动化（SMT、大模型辅助定理证明、分离逻辑、Horn子句求解等），
3、程序验证（C/Rust程序内存安全性验证等）。

081202-计算机软件与理论

计算机软硬件基础设施形式化验证，约束求解，程序验证

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,中科院自动化所中法信息、自动化与应用数学联合实验室, 博士后

2024-01-31-2028-01-30,中国计算机学会形式化方法专委会秘书长,

离散数学
离散数学（习题课）
计算机算法设计与分析
自动机理论及其应用

   

（1） An efficient string solver for string constraints with regex-counting and string-length, Journal of System Architecture, 2025, 第 2 作者  通讯作者
（2） Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks, FORMAL METHODS, PT II, FM 2024, 2025, 第 5 作者
（3） Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps, Formal Aspects of Computing, 2025, 第 2 作者  通讯作者
（4） Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once, DAC 2024, 2024, 第 6 作者  通讯作者
（5） A Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints, Acta Informatica, 2024, 第 3 作者
（6） Formal Verification of RISC-V Processor Chisel Designs, SETTA 2024, 2024, 第 5 作者
（7） SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits, TRANSACTIONS ON CRYPTOGRAPHIC HARDWARE AND EMBEDDED SYSTEMS, 2024, 第 5 作者
（8） 完备神经网络验证加速技术综述, Survey on Acceleration Techniques for Complete Neural Network Verification, 软件学报, 2024, 第 4 作者
（9） 前馈神经网络和循环神经网络的鲁棒性验证综述, Survey on Robustness Verification of Feedforward Neural Networks and Recurrent Neural Networks, 软件学报, 2023, 第 4 作者
（10） 芯片设计形式验证, Formal Verification of Circuit Design, 前瞻科技, 2023, 第 2 作者
（11） COMPSPEN：对形状性质与数据约束进行融合推理的分离逻辑求解器, COMPSPEN:Separation Logic Solver for Integrated Reasoning about Shape Properties and Data Constraints, 软件学报, 2023, 第 4 作者
（12） Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper), SEFM 2022, 2022, 第 5 作者
（13） Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables, POPL 2022, 2022, 第 9 作者  通讯作者
（14） Solving Not-Substring Constraint withFlat Abstraction, APLAS 2021, 2021, 第 8 作者  通讯作者
（15） Monadic Decomposition in Integer Linear Arithmetic, IJCAR 2020, 2020, 第 4 作者
（16） A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type, ATVA 2020, 2020, 第 7 作者
（17） Computing Linear Arithmetic Representation of Reachability Relation of One-counter Automata, SETTA 2020, 2020, 第 1 作者
（18） Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps, APLAS 2019, 2019, 第 4 作者  通讯作者
（19） Decision procedures for path feasibility of string-manipulating programs with complex operations, POPL 2019, 2019, 第 5 作者
（20） Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints, SOFSEM 2019, 2019, 第 3 作者  通讯作者
（21） Android Stack Machine, CAV 2018, 2018, 第 5 作者  通讯作者
（22） Register automata with linear arithmetic, LICS 2017, 2017, 第 4 作者
（23） What is decidable about string constraints with the ReplaceAll function, 第45届ACM 编程语言原则研讨会 (POPL), 2017, 第 5 作者
（24） Tractability of separation logic with inductive definitions: Beyond lists, International Conference on Concurrency Theory (CONCUR), 2017, 第 3 作者
（25） The Complexity of SORE-definability Problem, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), 2017, 第 1 作者
（26） Formal Reasoning on Infinite Data Values: An Ongoing Quest, ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016), 2017, 第 3 作者  通讯作者
（27） Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints, AUTOMATED DEDUCTION - CADE 26, 2017, 第 3 作者  通讯作者
（28） Verifying pushdown multi-agent systems against strategy logics, International Joint Conference on Artificial Intelligence (IJCAI 2016), 2016, 第 3 作者  通讯作者
（29） On temporal logics with data variable quantifications: Decidability and complexity, INFORMATION AND COMPUTATION, 2016, 第 2 作者  通讯作者
（30） Global Model Checking on Pushdown Multi-Agent Systems, 30th Association-for-the-Advancement-of-Artificial-Intelligence (AAAI) Conference on Artificial Intelligence, 2016, 第 3 作者
（31） 面向无穷数据的形式模型综述, Survey on Formal Models to Reason about Infinite Data Values, 软件学报, 2016, 第 2 作者
（32） Semipositivity in Separation Logic with Two Variables, DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, 2016, 第 1 作者  通讯作者
（33） The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach, COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 第 3 作者
（34） A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, AUTOMATED REASONING (IJCAR 2016), 2016, 第 3 作者  通讯作者
（35） On the Satisfiability of Indexed Linear Temporal Logics, 26th International Conference on Concurrency Theory (CONCUR 2015), 2015, 第 3 作者  通讯作者
（36） On Automated Lemma Generation for Separation Logic with Inductive Definitions, AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 第 3 作者
（37） On effective construction of the greatest solution of language inequality $XA \subseteq BX$, Theoretical Computer Science, 2014, 第 1 作者  通讯作者
（38） Extending Temporal Logics with Data Variable Quantifications, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), 2014, 第 1 作者  通讯作者
（39） Recursive queries on trees and data trees, The 16th International Conference on Database Theory (ICDT 2013), 2013, 第 1 作者  通讯作者
（40） A Decidable Extension of Data Automata, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, 第 1 作者
（41） Feasibility of motion planning on acyclic and strongly connected directed graphs, DISCRETE APPLIED MATHEMATICS, 2010, 第 1 作者  通讯作者
（42） Logical Locality Entails Frugal Distributed Computation over Graphs, GRAPH-THEORETIC CONCEPTS IN COMPUTER SCIENCE, 2010, 第 2 作者
（43） 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, 第 1 作者
（44） Feasibility of Motion Planning on Directed Graphs, THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, 2009, 第 1 作者
（45） 命题线性时序逻辑的对偶模型问题的复杂性, The Complexity of Dual Models Problem of Propositional Linear Temporal Logics, 软件学报, 2007, 第 1 作者
（46） A note on the characterization of tlef, INFORMATION PROCESSING LETTERS, 2007, 第 1 作者  通讯作者
（47） 命题线性时序逻辑的对偶模型问题的复杂性, The Complexity of Dual Models Problem of Propositional Linear Temporal Logics, 软件学报, 2007, 第 1 作者
（48） On the expressive power of qltl, 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007), 2007, 第 1 作者
（49） Quasi-star-free languages on infinite words, ACTA CYBERNETICA, 2005, 第 1 作者  通讯作者
（50） UML的形式化及其应用, 计算机科学, 2005, 第 4 作者
（51） Commutative Data Automata, CEUR, 第 1 作者

与国内外同行有广泛合作。国外合作包括：
 -- 法国：巴黎七大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/），利物浦大学的Tony Tan博士，https://www.liverpool.ac.uk/people/tony-tan

-- 德国：TU Kaiserslautern的Anthony W. Lin博士（https://anthonywlin.github.io/），University of Regensburg的Philipp Ruemmer博士（http://www.philipp.ruemmer.org/）

-- 捷克：Brno University of Technology的Ondrej Lengal博士（https://www.fit.vutbr.cz/~lengal/）、Lukas Holik博士

-- 中国台湾：中央研究院资讯研究所的陈郁方博士（https://www.iis.sinica.edu.tw/pages/yfc/）

   

已指导学生

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

陈艳  硕士研究生  081202-计算机软件与理论  

高冲  硕士研究生  081202-计算机软件与理论  

苏婉昀  硕士研究生  081202-计算机软件与理论  

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

何锦龙  博士研究生  081202-计算机软件与理论  

秦天航  硕士研究生  085405-软件工程  

现指导学生

冯维直  博士研究生  081202-计算机软件与理论  

于世禛  博士研究生  081200-计算机科学与技术  

迟智名  博士研究生  081200-计算机科学与技术  

胡登杭  博士研究生  081200-计算机科学与技术  

王修渊  硕士研究生  085405-软件工程  

董一凡  硕士研究生  081200-计算机科学与技术  

翁一平  硕士研究生  081200-计算机科学与技术  

朱雨田  博士研究生  081200-计算机科学与技术  

高华健  硕士研究生  081200-计算机科学与技术  

申世东  硕士研究生  081200-计算机科学与技术  

康跃馨  博士研究生  081200-计算机科学与技术  

肖扬  硕士研究生  081200-计算机科学与技术  

王远  博士研究生  081200-计算机科学与技术