| 2026 | ESOP | A Formally Verified Procedure for Width Inference in FIRRTL. | Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen |
| 2026 | FM | Can LLM Aid in Solving Constraints with Inductive Definitions? | Weizhi Feng, Shidong Shen, Jiaxiang Liu, Taolue Chen, Fu Song, Zhilin Wu |
| 2025 | APLAS | Decision Procedure for a Theory of String Sequences. | Denghang Hu, Taolue Chen, Philipp Rmmer, Fu Song, Zhilin Wu |
| 2025 | FMCAD | OSTRICH2: Solver for Complex String Constraints. | Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rmmer, Zhilin Wu |
| 2025 | ICCAD | BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing. | Shidong Shen, Jinyu Liu, Weizhi Feng, Fu Song, Zhilin Wu |
| 2025 | SETTA | Separation Logic with Heap Variables: A Decision Procedure and Its Application. | Xie Li, Yutian Zhu, Taolue Chen, Fu Song, Zhilin Wu |
| 2024 | DAC | Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. | Weizhi Feng, Yicheng Liu, Jiaxiang Liu, David N. Jansen, Lijun Zhang, Zhilin Wu |
| 2024 | DSN | Verifying Randomized Consensus Protocols with Common Coins. | Song Gao, Bohua Zhan, Zhilin Wu, Lijun Zhang |
| 2024 | FM | Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks. | Huiyu Tan, Xi Yang, Fu Song, Taolue Chen, Zhilin Wu |
| 2024 | SETTA | Formal Verification of RISC-V Processor Chisel Designs. | Shidong Shen, Yicheng Liu, Lijun Zhang, Fu Song, Zhilin Wu |
| 2023 | SETTA | String Constraints with Regex-Counting and String-Length Solved More Efficiently. | Denghang Hu, Zhilin Wu |
| 2022 | SEFM | CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). | Shizhen Yu, Yifan Dong, Jiuyang Liu, Yong Li, Zhilin Wu, David N. Jansen, Lijun Zhang |
| 2021 | APLAS | Solving Not-Substring Constraint withFlat Abstraction. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luks Holk, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen |
| 2020 | ATVA | A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. | Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rmmer, Zhilin Wu |
| 2020 | CADE | Monadic Decomposition in Integer Linear Arithmetic. | Matthew Hague, Anthony W. Lin, Philipp Rmmer, Zhilin Wu |
| 2020 | SETTA | Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata. | Xie Li, Taolue Chen, Zhilin Wu, Mingji Xia |
| 2019 | APLAS | Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. | Jinlong He, Taolue Chen, Ping Wang, Zhilin Wu, Jun Yan |
| 2019 | SOFSEM | Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. | Chong Gao, Taolue Chen, Zhilin Wu |
| 2019 | TACAS | SL-COMP: Competition of Solvers for Separation Logic. | Mihaela Sighireanu, Juan Antonio Navarro Prez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Toms Vojnar, Constantin Enea, Ondrej Lengl, Chong Gao, Zhilin Wu |
| 2018 | CAV | Android Stack Machine. | Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan |
| 2017 | CADE | Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. | Zhaowei Xu, Taolue Chen, Zhilin Wu |
| 2017 | CONCUR | Tractability of Separation Logic with Inductive Definitions: Beyond Lists. | Taolue Chen, Fu Song, Zhilin Wu |
| 2017 | ICFEM | Model Checking Pushdown Epistemic Game Structures. | Taolue Chen, Fu Song, Zhilin Wu |
| 2017 | LICS | Register automata with linear arithmetic. | Yu-Fang Chen, Ondrej Lengl, Tony Tan, Zhilin Wu |
| 2017 | MFCS | The Complexity of SORE-definability Problems. | Ping Lu, Zhilin Wu, Haiming Chen |
| 2016 | AAAI | Global Model Checking on Pushdown Multi-Agent Systems. | Taolue Chen, Fu Song, Zhilin Wu |
| 2016 | CADE | A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. | Xincai Gu, Taolue Chen, Zhilin Wu |
| 2016 | CAV | The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. | Yu-Fang Chen, Lei Song, Zhilin Wu |
| 2016 | IJCAI | Verifying Pushdown Multi-Agent Systems against Strategy Logics. | Taolue Chen, Fu Song, Zhilin Wu |
| 2016 | SETTA | Semipositivity in Separation Logic with Two Variables. | Zhilin Wu |
| 2015 | ATVA | On Automated Lemma Generation for Separation Logic with Inductive Definitions. | Constantin Enea, Mihaela Sighireanu, Zhilin Wu |
| 2015 | CONCUR | On the Satisfiability of Indexed Linear Temporal Logics. | Taolue Chen, Fu Song, Zhilin Wu |
| 2013 | ICDT | Recursive queries on trees and data trees. | Serge Abiteboul, Pierre Bourhis, Anca Muscholl, Zhilin Wu |
| 2012 | CSL | Commutative Data Automata. | Zhilin Wu |
| 2009 | TAMC | Feasibility of Motion Planning on Directed Graphs. | Zhilin Wu, Stphane Grumbach |
| 2009 | WG | Logical Locality Entails Frugal Distributed Computation over Graphs (Extended Abstract). | Stphane Grumbach, Zhilin Wu |
| 2007 | ICTAC | On the Expressive Power of QLTL. | Zhilin Wu |
| 2004 | ICASSP | Inner lip feature extraction for MPEG-4 facial animation. | Zhilin Wu, Petar S. Aleksic |
| 2002 | ICIP | Audio-visual continuous speech recognition using MPEG-4 compliant visual features. | Petar S. Aleksic, Jay J. Williams, Zhilin Wu, Aggelos K. Katsaggelos |
| 2002 | ICMI | Lip Tracking for MPEG-4 Facial Animation. | Zhilin Wu, Petar S. Aleksic, Aggelos K. Katsaggelos |