计算机软硬件系统的形式化验证，计算逻辑，自动机理论

如果你是一名对以下方向感兴趣的高年级本科生，欢迎联系我（包括实习、硕士研究生保送推荐与考试）。
1、计算机软硬件系统的形式化验证（操作系统验证、编译器验证、C/Rust程序内存安全性验证等），
2、计算逻辑（比如时序逻辑、分离逻辑、字符串约束等），
3、自动机理论（比如正规表达式、有限自动机、下推自动机、存储自动机等）。
更多信息请访问个人主页：http://lcs.ios.ac.cn/~wuzl

081202-计算机软件与理论
085400-电子信息

对以下类型程序的自动分析与验证：操作字符串的程序、Android程序、深度神经网络、操作操作动态数据结构的程序、大数据流处理程序

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

2016-01-25-2020-12-30,中国计算机学会形式化方法专业组成员,

离散数学
自动机理论及其应用

这是一门针对中科院软件所博士生的专业基础课程。

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

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

   

（1） CCF-IEEE青年科学家奖, 其他, 2020

[1] 刘易铖, 冯维直, 吴志林, 张立军. RISC-V处理器Chisel设计指令集一致性的形式验证方法及装置. CN: CN116701085A, 2023-09-05.
[2] 许颖, 康跃馨, 陈胜, 夏清, 方明哲, 吴志林, 李玉成. 用于翻译智能合约语言的方法和装置、电子设备. CN: CN116149671B, 2023-07-04.
[3] 于世禛, 董一凡, 李勇, 吴志林, 杨大卫, 张立军. Chisel断言语言的类SVA扩展及形式化验证方法. CN 115496017 B, 2023-04-11.
[4] 于世禛, 董一凡, 李勇, 吴志林, 杨大卫, 张立军. Chisel断言语言的类SVA扩展及形式化验证方法. CN: CN115496017B, 2023-04-11.
[5] 于世禛, 董一凡, 李勇, 吴志林, 杨大卫, 张立军. Chisel断言语言的类SVA扩展及形式化验证方法. CN: CN115496017A, 2022-12-20.

   

（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 作者

   

（ 1 ） 无穷字母表上的形式模型：逻辑与自动机, 负责人, 国家任务, 2012-01--2014-12
（ 2 ） 符号模型与隐式模型检测技术, 参与, 国家任务, 2013-01--2016-12
（ 3 ） 动态数据结构的形状性质与数据约束：基于分离逻辑的自动分析与验证, 负责人, 国家任务, 2015-01--2018-12
（ 4 ） 同步数据流模型优化研究, 参与, 国家任务, 2016-01--2019-12
（ 5 ） 分布式流处理程序的分析与验证, 负责人, 国家任务, 2019-01--2022-12
（ 6 ） 内生安全应用构造技术, 负责人, 国家任务, 2019-04--2020-12
（ 7 ） 高安全可靠网络系统形式建模与生成技术委托合同, 负责人, 国家任务, 2020-02--2023-12
（ 8 ） JavaScript污点分析引擎前端模块技术, 负责人, 境内委托项目, 2021-06--2022-05
（ 9 ） 智能合约高效执行引擎及新型指令集, 负责人, 国家任务, 2022-11--2025-10
（ 10 ） 面向RISC-V的形式化验证技术与工具, 负责人, 中国科学院计划, 2022-12--2025-12

与国内外同行有广泛合作。国外合作包括：
 -- 法国：巴黎七大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/）

-- 德国：TU Kaiserslautern的Anthony W. Lin博士（https://anthonywlin.github.io/）

-- 瑞典：Uppsala University大学的Philipp Ruemmer博士（http://www.philipp.ruemmer.org/）

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

-- 台湾：中央研究院资讯研究所的陈郁方博士（https://www.iis.sinica.edu.tw/pages/yfc/）、National Taiwan University的Tony Tan博士(https://www.csie.ntu.edu.tw/~tonytan/)

   

已指导学生

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

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

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

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

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

现指导学生

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

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

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

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

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

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

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

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

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

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