Audio-visual continuous speech recognition using MPEG-4 compliant visual features. - Petar S. Aleksic; Jay J. Williams; Zhilin Wu; Aggelos K. Katsaggelos (ICIP (1), 2002)

Lip Tracking for MPEG-4 Facial Animation. - Zhilin Wu; Petar S. Aleksic; Aggelos K. Katsaggelos (ICMI, 2002)

Audio-Visual Speech Recognition Using MPEG-4 Compliant Visual Features. - Petar S. Aleksic; Jay J. Williams; Zhilin Wu; Aggelos K. Katsaggelos (EURASIP J. Adv. Signal Process., 2002)

Inner lip feature extraction for MPEG-4 facial animation. - Zhilin Wu; Petar S. Aleksic (ICASSP (3), 2004)

A Formal Framework of UML. - Jin Zhou; Yinglong Ma 001; Wei Li 038; Zhilin Wu (Software Engineering Research and Practice, 2004)

MPEG-4 outer-inner lip FAP interpolation. - Zhilin Wu; Aggelos K. Katsaggelos; Thrasyvoulos N. Pappas (Electronic Imaging: Image and Video Communications and Processing, 2005)

Quasi-star-free Languages on Infinite Words. - Zhilin Wu (Acta Cybern., 2005)

On the Expressive Power of QLTL. - Zhilin Wu (ICTAC, 2007)

A note on the characterization of TL[EF]. - Zhilin Wu (Inf. Process. Lett., 2007)

Feasibility of Motion Planning on Directed Graphs. - Zhilin Wu; Stéphane Grumbach (TAMC, 2009)

Logical Locality Entails Frugal Distributed Computation over Graphs (Extended Abstract). - Stéphane Grumbach; Zhilin Wu (WG, 2009)

On Distributed Model Checking of MSO on Graphs - Stéphane Grumbach; Zhilin Wu (CoRR, 2009)

Logical locality entails frugal distributed computation over graphs - Stéphane Grumbach; Zhilin Wu (CoRR, 2009)

On the distributed evaluation of recursive queries over graphs - Stéphane Grumbach; Fang Wang; Zhilin Wu (CoRR, 2009)

Verifying Recursive Active Documents with Positive Data Tree Rewriting. - Blaise Genest; Anca Muscholl; Zhilin Wu (FSTTCS, 2010)

Distributed tree decomposition of graphs and applications to verification. - Stéphane Grumbach; Zhilin Wu (IPDPS Workshops, 2010)

Feasibility of motion planning on acyclic and strongly connected directed graphs. - Zhilin Wu; Stéphane Grumbach (Discret. Appl. Math., 2010)

A Decidable Extension of Data Automata - Zhilin Wu (GandALF, 2011)

Commutative Data Automata. - Zhilin Wu (CSL, 2012)

On Injective Embeddings of Tree Patterns - Jakub Michaliszyn; Anca Muscholl; Slawek Staworko; Piotr Wieczorek; Zhilin Wu (CoRR, 2012)

Recursive queries on trees and data trees. - Serge Abiteboul; Pierre Bourhis; Anca Muscholl; Zhilin Wu (ICDT, 2013)

Extending Temporal Logics with Data Variable Quantifications. - Fu Song; Zhilin Wu (FSTTCS, 2014)

Regular path queries on graphs with data: A rigid approach. - Zhilin Wu (CoRR, 2014)

On effective construction of the greatest solution of language inequality XA ⊆ BX. - Olivier Ly; Zhilin Wu (Theor. Comput. Sci., 2014)

On Automated Lemma Generation for Separation Logic with Inductive Definitions. - Constantin Enea; Mihaela Sighireanu; Zhilin Wu (ATVA, 2015)

On the Satisfiability of Indexed Linear Temporal Logics. - Taolue Chen 001; Fu Song; Zhilin Wu (CONCUR, 2015)

Global Model Checking on Pushdown Multi-Agent Systems. - Taolue Chen 001; Fu Song; Zhilin Wu (AAAI, 2016)

A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. - Xincai Gu; Taolue Chen 001; Zhilin Wu (IJCAR, 2016)

The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. - Yu-Fang Chen 001; Lei Song; Zhilin Wu (CAV (2), 2016)

Verifying Pushdown Multi-Agent Systems against Strategy Logics. - Taolue Chen 001; Fu Song; Zhilin Wu (IJCAI, 2016)

Formal Reasoning on Infinite Data Values: An Ongoing Quest. - Taolue Chen 001; Fu Song; Zhilin Wu (SETSS, 2016)

Semipositivity in Separation Logic with Two Variables. - Zhilin Wu (SETTA, 2016)

On temporal logics with data variable quantifications: Decidability and complexity. - Fu Song; Zhilin Wu (Inf. Comput., 2016)

Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. - Zhaowei Xu; Taolue Chen 001; Zhilin Wu (CADE, 2017)

Tractability of Separation Logic with Inductive Definitions: Beyond Lists. - Taolue Chen 001; Fu Song; Zhilin Wu (CONCUR, 2017)

Model Checking Pushdown Epistemic Game Structures. - Taolue Chen 001; Fu Song; Zhilin Wu (ICFEM, 2017)

Register automata with linear arithmetic. - Yu-Fang Chen 001; Ondrej Lengál; Tony Tan; Zhilin Wu (LICS, 2017)

The Complexity of SORE-definability Problems. - Ping Lu 007; Zhilin Wu; Haiming Chen 001 (MFCS, 2017)

Android Stack Machine. - Taolue Chen 001; Jinlong He; Fu Song; Guozhen Wang; Zhilin Wu; Jun Yan (CAV (2), 2018)

What is decidable about string constraints with the ReplaceAll function. - Taolue Chen 001; Yan Chen; Matthew Hague; Anthony W. Lin; Zhilin Wu (Proc. ACM Program. Lang., 2018)

Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. - Jinlong He; Taolue Chen 001; Ping Wang; Zhilin Wu; Jun Yan (APLAS, 2019)

Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. - Chong Gao; Taolue Chen 001; Zhilin Wu (SOFSEM, 2019)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

Decision procedures for path feasibility of string-manipulating programs with complex operations. - Taolue Chen 001; Matthew Hague; Anthony W. Lin; Philipp Rümmer; Zhilin Wu (Proc. ACM Program. Lang., 2019)

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. - Taolue Chen 001; Matthew Hague; Jinlong He; Denghang Hu; Anthony Widjaja Lin; Philipp Rümmer; Zhilin Wu (ATVA, 2020)

Monadic Decomposition in Integer Linear Arithmetic. - Matthew Hague; Anthony W. Lin; Philipp Rümmer; Zhilin Wu (IJCAR (1), 2020)

Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata. - Xie Li; Taolue Chen 001; Zhilin Wu; Mingji Xia (SETTA, 2020)

Monadic Decomposition in Integer Linear Arithmetic (Technical Report). - Matthew Hague; Anthony Widjaja Lin; Philipp Rümmer; Zhilin Wu (CoRR, 2020)

Solving Not-Substring Constraint withFlat Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Denghang Hu; Wei-Lun Tsai; Zhilin Wu; Di-De Yen (APLAS, 2021)

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). - Shizhen Yu; Yifan Dong; Jiuyang Liu; Yong Li 031; Zhilin Wu; David N. Jansen; Lijun Zhang 001 (SEFM, 2022)

Solving string constraints with Regex-dependent functions through transducers with priorities and variables. - Taolue Chen 001; Alejandro Flores-Lamas; Matthew Hague; Zhilei Han; Denghang Hu; Shuanglong Kan; Anthony W. Lin; Philipp Rümmer; Zhilin Wu (Proc. ACM Program. Lang., 2022)

String Constraints with Regex-Counting and String-Length Solved More Efficiently. - Denghang Hu; Zhilin Wu (SETTA, 2023)

SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits. - Huiyu Tan; Pengfei Gao; Taolue Chen 001; Fu Song; Zhilin Wu (CoRR, 2023)

Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. - Weizhi Feng; Yicheng Liu; Jiaxiang Liu 001; David N. Jansen; Lijun Zhang 001; Zhilin Wu (DAC, 2024)

Verifying Randomized Consensus Protocols with Common Coins. - Song Gao 014; Bohua Zhan; Zhilin Wu; Lijun Zhang 001 (DSN, 2024)

Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks. - Huiyu Tan; Xi Yang; Fu Song; Taolue Chen 001; Zhilin Wu (FM (2), 2024)

Formal Verification of RISC-V Processor Chisel Designs. - Shidong Shen; Yicheng Liu; Lijun Zhang 001; Fu Song; Zhilin Wu (SETTA, 2024)

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions. - Wanyun Su; Zhilin Wu; Mihaela Sighireanu (CoRR, 2024)

SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits. - Huiyu Tan; Pengfei Gao; Fu Song; Taolue Chen 001; Zhilin Wu (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

A decision procedure for string constraints with string/integer conversion and flat regular constraints. - Hao Wu 085; Yu-Fang Chen 001; Zhilin Wu; Bican Xia; Naijun Zhan (Acta Informatica, 2024)

HKSCSO: A Novel Enhanced Sand Cat Swarm Optimization Algorithm for UAV Three-Dimensional Path Planning. - Kang Wang; Xin Zeng; Sujie Xian; Zhongxin Li; Zhilin Wu (Concurr. Comput. Pract. Exp., 2025)

ODE-DSN: A surrogate model for dynamic stiffness in microscopic RVE problems under nonuniform time-step strain inputs. - Kai Xie; Yongqing Huo; Zhongxin Li; Zhilin Wu (J. Comput. Des. Eng., 2025)

An efficient string solver for string constraints with regex-counting and string-length. - Denghang Hu; Zhilin Wu (J. Syst. Archit., 2025)

OSTRICH2: Solver for Complex String Constraints. - Matthew Hague; Denghang Hu; Artur Jez; Anthony W. Lin; Oliver Markgraf; Philipp Rümmer; Zhilin Wu (CoRR, 2025)

Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps. - Jinlong He; Zhilin Wu; Taolue Chen 001 (Formal Aspects Comput., 2025)

Towards Large Language Model-Friendly APls. - Yuan Wang; Zhenyuan Yang; Zhanbo Wang; Mingyu Li; Zhilin Wu; Haibo Chen (ACM SIGOPS Oper. Syst. Rev., 2025)