发表论文(除极特殊情况外,论文作者均以姓名字母序排列)
(1) Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once, DAC 2024, 2024, 第 1 作者(2) 前馈神经网络和循环神经网络的鲁棒性验证综述, Survey on Robustness Verification of Feedforward Neural Networks and Recurrent Neural Networks, 软件学报, 2023, 第 4 作者(3) 芯片设计形式验证, Formal Verification of Circuit Design, 前瞻科技, 2023, 第 2 作者(4) A Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints, Acta Informatica, 2023, 第 3 作者(5) Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper), SEFM 2022, 2022, 第 5 作者(6) Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables, POPL 2022, 2022, 通讯作者(7) Solving Not-Substring Constraint withFlat Abstraction, APLAS 2021, 2021, 通讯作者(8) Monadic Decomposition in Integer Linear Arithmetic, IJCAR 2020, 2020, 第 4 作者(9) A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type, ATVA 2020, 2020, 第 7 作者(10) Computing Linear Arithmetic Representation of Reachability Relation of One-counter Automata, Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA 2020), 2020, 第 1 作者(11) Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps, PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2019, 2019, 通讯作者(12) Decision procedures for path feasibility of string-manipulating programs with complex operations, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES, 2019, 第 5 作者(13) Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints, THEORY AND PRACTICE OF COMPUTER SCIENCE, SOFSEM 2019, 2019, 通讯作者(14) Android Stack Machine, COMPUTER AIDED VERIFICATION, CAV 2018, PT II, 2018, 通讯作者(15) Register automata with linear arithmetic, 2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017, 第 4 作者(16) What is decidable about string constraints with the ReplaceAll function, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES, 2017, 第 5 作者(17) Tractability of separation logic with inductive definitions: Beyond lists, International Conference on Concurrency Theory (CONCUR), 2017, 第 1 作者(18) The Complexity of SORE-definability Problem, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), 2017, 第 1 作者(19) Formal Reasoning on Infinite Data Values: An Ongoing Quest, ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016), 2017, 通讯作者(20) Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints, AUTOMATED DEDUCTION - CADE 26, 2017, 通讯作者(21) Verifying pushdown multi-agent systems against strategy logics, International Joint Conference on Artificial Intelligence (IJCAI 2016), 2016, 通讯作者(22) On temporal logics with data variable quantifications: Decidability and complexity, INFORMATION AND COMPUTATION, 2016, 通讯作者(23) Global Model Checking on Pushdown Multi-Agent Systems, THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, 第 3 作者(24) 面向无穷数据的形式模型综述, Survey on Formal Models to Reason about Infinite Data Values, 软件学报, 2016, 第 2 作者(25) Semipositivity in Separation Logic with Two Variables, DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, 2016, 通讯作者(26) The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach, COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 第 3 作者(27) A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, AUTOMATED REASONING (IJCAR 2016), 2016, 通讯作者(28) On the Satisfiability of Indexed Linear Temporal Logics, 26th International Conference on Concurrency Theory (CONCUR 2015), 2015, 通讯作者(29) On Automated Lemma Generation for Separation Logic with Inductive Definitions, AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 第 3 作者(30) On effective construction of the greatest solution of language inequality $XA \subseteq BX$, Theoretical Computer Science, 2014, 通讯作者(31) Extending Temporal Logics with Data Variable Quantifications, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), 2014, 通讯作者(32) Recursive queries on trees and data trees, The 16th International Conference on Database Theory (ICDT 2013), 2013, 通讯作者(33) A Decidable Extension of Data Automata, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, 第 1 作者(34) Feasibility of motion planning on acyclic and strongly connected directed graphs, DISCRETE APPLIED MATHEMATICS, 2010, 通讯作者(35) Logical Locality Entails Frugal Distributed Computation over Graphs, GRAPH-THEORETIC CONCEPTS IN COMPUTER SCIENCE, 2010, 第 2 作者(36) 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 作者(37) Feasibility of Motion Planning on Directed Graphs, THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, 2009, 第 1 作者(38) 命题线性时序逻辑的对偶模型问题的复杂性, The Complexity of Dual Models Problem of Propositional Linear Temporal Logics, 软件学报, 2007, 第 1 作者(39) A note on the characterization of tlef, INFORMATION PROCESSING LETTERS, 2007, 通讯作者(40) 命题线性时序逻辑的对偶模型问题的复杂性, The Complexity of Dual Models Problem of Propositional Linear Temporal Logics, 软件学报, 2007, 第 1 作者(41) On the expressive power of qltl, LECTURE NOTES IN COMPUTER SCIENCE (INCLUDING SUBSERIES LECTURE NOTES IN ARTIFICIAL INTELLIGENCE AND LECTURE NOTES IN BIOINFORMATICS), 2007, 第 1 作者(42) Quasi-star-free languages on infinite words, ACTA CYBERNETICA, 2005, 通讯作者(43) UML的形式化及其应用, 计算机科学, 2005, 第 4 作者(44) Commutative Data Automata, CEUR, 第 1 作者