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

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

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） CCF-IEEE青年科学家奖, 其他, 2020

（ 1 ） RISC-V处理器Chisel设计指令集一致性的形式验证方法及装置, 发明专利, 2023, 第 3 作者, 专利号: CN116701085A

（ 2 ） 用于翻译智能合约语言的方法和装置、电子设备, 2023, 第 6 作者, 专利号: CN116149671B

（ 3 ） Chisel断言语言的类SVA扩展及形式化验证方法, 发明专利, 2023, 第 4 作者, 专利号: CN 115496017 B

（ 4 ） Chisel断言语言的类SVA扩展及形式化验证方法, 发明专利, 2022, 第 4 作者, 专利号: CN115496017A

（ 5 ） Chisel断言语言的类SVA扩展及形式化验证方法, 2023, 第 4 作者, 专利号: CN115496017B

   

[1] 吴志林, Weizhi Feng, Yicheng Liu, Jiaxiang Liu, David N. Jansen, Zhang, Lijun. Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. DAC 2024null. 2024, [2] 刘颖, 杨鹏飞, 张立军, 吴志林, 冯元. 前馈神经网络和循环神经网络的鲁棒性验证综述. 软件学报. 2023, 34(7): 3134-3166, http://lib.cqvip.com/Qikan/Article/Detail?id=7110099236.
[3] 詹博华, 吴志林. 芯片设计形式验证. 前瞻科技. 2023, 2(1): 23-32, http://lib.cqvip.com/Qikan/Article/Detail?id=7109340606.
[4] Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, 詹乃军. A Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints. Acta Informatica[J]. 2023, [5] 于世禛, 董一凡, 刘玖阳, 李勇, 吴志林, David N. Jansen, 张立军. Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). SEFM 2022null. 2022, [6] Chen, Taolue, Lamas, Alejandro Flores, Hague, Matthew, Han, Zhilei, 胡登杭, Kan, Shuanglong, Lin, Anthony Widjaja, Ruemmer, Philipp, Wu, Zhilin. Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. POPL 2022null. 2022, [7] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, 胡登杭, Wei-Lun Tsai, 吴志林, Di-De Yen. Solving Not-Substring Constraint withFlat Abstraction. APLAS 2021null. 2021, [8] Matthew Hague, Anthony W Lin, Philipp Rmmer, Zhilin Wu. Monadic Decomposition in Integer Linear Arithmetic. IJCAR 2020null. 2020, 12166: 122-140, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324128/.
[9] Chen Taolue, Hague Matthew, He Jinlong, Hu Denghang, Lin Anthony Widjaja, Rummer Philipp, Wu Zhilin. A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. ATVA 2020null. 2020, http://arxiv.org/abs/2007.06913.
[10] 吴志林. Computing Linear Arithmetic Representation of Reachability Relation of One-counter Automata. Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA 2020)null. 2020, [11] He, Jinlong, Chen, Taolue, Wang, Ping, Wu, Zhilin, Yan, Jun, Lin, AW. Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2019null. 2019, 11893: 291-312, [12] Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rmmer, Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGESnull. 2019, 3: [13] Gao, Chong, Chen, Taolue, Wu, Zhilin, Catania, B, Kralovic, R, Nawrocki, J, Pighizzini, G. Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. THEORY AND PRACTICE OF COMPUTER SCIENCE, SOFSEM 2019null. 2019, 11376: 206-220, [14] Chen Taolue, He Jinlong, Song Fu, Wang Guozhen, Wu Zhilin, Yan Jun, Chockler H, Weissenbacher G. Android Stack Machine. COMPUTER AIDED VERIFICATION, CAV 2018, PT IInull. 2018, 10982: 487-504, [15] Chen, YuFang, Lengal, Ondrej, Tan, Tony, Wu, Zhilin, IEEE. Register automata with linear arithmetic. 2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)null. 2017, [16] Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, Zhilin Wu. What is decidable about string constraints with the ReplaceAll function. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGESnull. 2017, 2: [17] 吴志林. Tractability of separation logic with inductive definitions: Beyond lists. International Conference on Concurrency Theory (CONCUR). 2017, [18] 吴志林. The Complexity of SORE-definability Problem. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). 2017, [19] Chen Taolue, Song Fu, Wu Zhilin, Bowen JP, Liu Z, Zhang Z. Formal Reasoning on Infinite Data Values: An Ongoing Quest. ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016)null. 2017, 10215: 195-257, [20] Xu Zhaowei, Chen Taolue, Wu Zhilin, DeMoura L. Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. AUTOMATED DEDUCTION - CADE 26null. 2017, 10395: 509-527, [21] 吴志林. Verifying pushdown multi-agent systems against strategy logics. International Joint Conference on Artificial Intelligence (IJCAI 2016). 2016, [22] Song, Fu, Wu, Zhilin. On temporal logics with data variable quantifications: Decidability and complexity. INFORMATION AND COMPUTATION[J]. 2016, 251: 104-139, http://dx.doi.org/10.1016/j.ic.2016.08.002.
[23] Chen Taolue, Song Fu, Wu Zhilin, AAAI. Global Model Checking on Pushdown Multi-Agent Systems. THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCEnull. 2016, 2459-2465, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000485474202070.
[24] 宋富, 吴志林. 面向无穷数据的形式模型综述. 软件学报[J]. 2016, 682-690, http://lib.cqvip.com/Qikan/Article/Detail?id=668151132.
[25] Wu Zhilin, Franzle M, Kapur D, Zhan N. Semipositivity in Separation Logic with Two Variables. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONSnull. 2016, 9984: 179-196, [26] Chen YuFang, Song Lei, Wu Zhilin, Chaudhuri S, Farzan A. The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT IInull. 2016, 9780: 91-111, [27] Gu Xincai, Chen Taolue, Wu Zhilin, Olivetti N, Tiwari A. A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. AUTOMATED REASONING (IJCAR 2016)null. 2016, 9706: 532-549, [28] 吴志林. On the Satisfiability of Indexed Linear Temporal Logics. 26th International Conference on Concurrency Theory (CONCUR 2015). 2015, [29] Enea Constantin, Sighireanu Mihaela, Wu Zhilin, Finkbeiner B, Pu G, Zhang L. On Automated Lemma Generation for Separation Logic with Inductive Definitions. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015null. 2015, 9364: 80-96, [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] Zhilin Wu. A Decidable Extension of Data Automata. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE[J]. 2011, 54: 116-130, https://doaj.org/article/2a327cc7c5954873ba11ea441dcc3f5f.
[34] Wu, Zhilin, Grumbach, Stephane. Feasibility of motion planning on acyclic and strongly connected directed graphs. DISCRETE APPLIED MATHEMATICS[J]. 2010, 158(9): 1017-1028, http://dx.doi.org/10.1016/j.dam.2010.02.001.
[35] Grumbach Stephane, Wu Zhilin, Paul C, Habib M. Logical Locality Entails Frugal Distributed Computation over Graphs. GRAPH-THEORETIC CONCEPTS IN COMPUTER SCIENCEnull. 2010, 5911: 154-165, [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, [37] Wu Zhilin, Grumbach Stephane, Chen J, Cooper SB. Feasibility of Motion Planning on Directed Graphs. THEORY AND APPLICATIONS OF MODELS OF COMPUTATIONnull. 2009, 5532: 430-439, [38] WU ZhiLin, ZHANG WenHui. 命题线性时序逻辑的对偶模型问题的复杂性. 软件学报[J]. 2007, 18(7): 1573-1581, http://lib.cqvip.com/Qikan/Article/Detail?id=24884665.
[39] Wu, Zhilin. A note on the characterization of TLEF. INFORMATION PROCESSING LETTERS[J]. 2007, 102(2-3): 48-54, http://www.corc.org.cn/handle/1471x/2380343.
[40] 吴志林, 张文辉. 命题线性时序逻辑的对偶模型问题的复杂性. 软件学报[J]. 2007, 18(7): 1573-1581, http://lib.cqvip.com/Qikan/Article/Detail?id=24884665.
[41] Wu Zhilin. On the expressive power of qltl. LECTURE NOTES IN COMPUTER SCIENCE (INCLUDING SUBSERIES LECTURE NOTES IN ARTIFICIAL INTELLIGENCE AND LECTURE NOTES IN BIOINFORMATICS)null. 2007, 467-481, http://124.16.136.157/handle/311060/11130.
[42] Wu Zhilin. Quasi-star-free Languages on Infinite Words. ACTA CYBERNETICA[J]. 2005, 17(1): 75-93, [43] 周瑾, 马应龙, 李巍, 吴志林. UML的形式化及其应用. 计算机科学[J]. 2005, 32(3): 136-140, http://lib.cqvip.com/Qikan/Article/Detail?id=15215066.
[44] Zhilin Wu. Commutative Data Automata. CEUR. http://oa.las.ac.cn/oainone/service/browseall/read1?ptype=CA&workid=CA201702140000157CD.

   

（ 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-计算机科学与技术