伍之琳｜长沙理工大学｜学者主页

2026

A Formally Verified Procedure for Width Inference in FIRRTL

Keyin Wang, Xiao-Mu Shi, Jia-Xiang Liu, Zhilin Wu, Taolue Chen, Fu Song, David N. Jansen

European Symposium on Programming

DOI

2026

χ RVFormal: Formal verification of RISC-V processor Chisel designs

Shidong Shen, Shi-Jie Chen, Yicheng Liu, Lijun Zhang, Fu Song, Zhilin Wu

Journal of systems architecture

DOI

2026

Can LLM Aid in Solving Constraints with Inductive Definitions?

Wei-Zhi Feng, Shidong Shen, Jia-Xiang Liu, Taolue Chen, Fu Song, Zhilin Wu

World Congress on Formal Methods

DOI

2026

Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction

Xi Yang, Tao Chen, Yuqi Chen, Fu Song, Chun-Dong Wang, Zhilin Wu

arXiv.org

DOI

2025

An efficient string solver for string constraints with regex-counting and string-length

Denghang Hu, Zhilin Wu

Journal of systems architecture

DOI

2025

Separation Logic with Heap Variables: A Decision Procedure and Its Application

Xie Li, Yu-Tian Zhu, Taolue Chen, Fu Song, Zhilin Wu

International Symposium on Software Engineering: Theories, Tools, and Applications

DOI

2025

OSTRICH2: Solver for Complex String Constraints

Matthew Hague, Denghang Hu, Artur Jeż, A. W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu

Formal Methods in Computer-Aided Design

DOI

2025

Decision Procedure for A Theory of String Sequences

Denghang Hu, Taolue Chen, Philipp Rümmer, Fu Song, Zhilin Wu

Asian Symposium on Programming Languages and Systems

DOI

2025

BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing

Shidong Shen, Jinyu Liu, Wei-Zhi Feng, Fu Song, Zhilin Wu

2025 IEEE/ACM International Conference On Computer Aided Design (ICCAD)

DOI

2024

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions

Wanyun Su, Zhilin Wu, M. Sighireanu

arXiv.org

DOI

2024

Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once

Wei-Zhi Feng, Yicheng Liu, Jia-Xiang Liu, David N. Jansen, Lijun Zhang, Zhilin Wu

Design Automation Conference

DOI

2024

Verifying Randomized Consensus Protocols with Common Coins

Song Gao, Bo-Hua Zhan, Zhilin Wu, Lijun Zhang

Dependable Systems and Networks

DOI

2024

Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks

Huiyu Tan, Xi Yang, Fu Song, Taolue Chen, Zhilin Wu

World Congress on Formal Methods

DOI

2024

SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits

Huiyu Tan, Pengfei Gao, Fu Song, Taolue Chen, Zhilin Wu

IACR Trans. Cryptogr. Hardw. Embed. Syst.

DOI

2024

Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps

Jinlong He, Zhilin Wu, Taolue Chen

Formal Aspects Comput.

DOI

2024

Formal Verification of RISC-V Processor Chisel Designs

Shidong Shen, Yicheng Liu, Lijun Zhang, Fu Song, Zhilin Wu

International Symposium on Software Engineering: Theories, Tools, and Applications

DOI

2023

基础设施投资能促进共同富裕吗

龙海明，伍之琳

《金融与经济》

2023

A decision procedure for string constraints with string/integer conversion and flat regular constraints

Hao Wu, Yu-Fang Chen, Zhilin Wu, Bi-Can Xia, Nai-Jun Zhan

Acta Informatica

DOI

2023

OSTRICH Version 1.3

Taolue Chen, Riccardo De Masellis, Alejandro Flores-Lamas, Matthew Hague, Zhi-Lei Han, Denghang Hu, A. W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu

2023

String Constraints with Regex-Counting and String-Length Solved More Efficiently

Denghang Hu, Zhilin Wu

International Symposium on Software Engineering: Theories, Tools, and Applications

DOI

2022

The OSTRICH String Solver

Taolue Chen, Riccardo De Masellis, Alejandro Flores-Lamas, M. Hague, Zhi-Lei Han, Denghang Hu, Shuanglong Kan, A. Lin, Oliver Markgraf, Philipp Rümmer, Amanda Stjerna, Zhilin Wu

2022

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper)

Shi-Zhen Yu, Yi-Fan Dong, Jiuyang Liu, Yong Li, Zhilin Wu, D. Jansen, Li-Jun Zhang

IEEE International Conference on Software Engineering and Formal Methods

DOI

2021

Solving Not-Substring Constraint withFlat Abstraction

P. Abdulla, M. Atig, Yu-Fang Chen, Diep Phi Bui, L. Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen

Asian Symposium on Programming Languages and Systems

DOI

2021

Solving string constraints with Regex-dependent functions through transducers with priorities and variables

Taolue Chen, Alejandro Flores-Lamas, M. Hague, Zhi-Lei Han, Denghang Hu, Shuanglong Kan, A. Lin, Philipp Rümmer, Zhilin Wu

Proc. ACM Program. Lang.

DOI

2020

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Taolue Chen, M. Hague, Jinlong He, Denghang Hu, A. Lin, Philipp Rümmer, Zhilin Wu

Automated Technology for Verification and Analysis

DOI

2020

Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata

Xie Li, Taolue Chen, Zhilin Wu, Mingji Xia

International Symposium on Software Engineering: Theories, Tools, and Applications

DOI

2020

Monadic Decomposition in Integer Linear Arithmetic

M. Hague, A. Lin, Philipp Rümmer, Zhilin Wu

International Joint Conference on Automated Reasoning

DOI

2019

Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps

Jinlong He, Taolue Chen, Ping Wang, Zhilin Wu, Jun Yan

Asian Symposium on Programming Languages and Systems

DOI

2019

SL-COMP: Competition of Solvers for Separation Logic

M. Sighireanu, J. A. Pérez, A. Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, T. Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, T. Le, Thanh-Toan Nguyen, Si-Au-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomáš Vojnar, C. Enea, Ondřej Lengál, Chong Gao, Zhilin Wu

International Conference on Tools and Algorithms for Construction and Analysis of Systems

DOI

2018

Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints

Chong Gao, Taolue Chen, Zhilin Wu

Conference on Current Trends in Theory and Practice of Informatics

DOI

2018

Android Stack Machine

Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan

International Conference on Computer Aided Verification

DOI

2018

Decision procedures for path feasibility of string-manipulating programs with complex operations

Taolue Chen, M. Hague, A. Lin, Philipp Rümmer, Zhilin Wu

Proc. ACM Program. Lang.

DOI

2018

OSTRICH String Constraint Solver and Results

Taolue Chen, M. Hague, A. Lin, Philipp Rümmer, Zhilin Wu

Artifact Digital Object Group

DOI

2017

Review of Equity Risk Premium Puzzle

伍之琳，宋晖

《怀化学院学报》

2017

What is decidable about string constraints with the ReplaceAll function

Taolue Chen, Yan Chen, M. Hague, Anthony W. Lin, Zhilin Wu

Proc. ACM Program. Lang.

DOI

2017

Tractability of Separation Logic with Inductive Definitions: Beyond Lists

Taolue Chen, Fu Song, Zhilin Wu

International Conference on Concurrency Theory

DOI

2017

The Complexity of SORE-definability Problems

Ping Lu, Zhilin Wu, H. Chen

International Symposium on Mathematical Foundations of Computer Science

DOI

2017

Model Checking Pushdown Epistemic Game Structures

Taolue Chen, Fu Song, Zhilin Wu

IEEE International Conference on Formal Engineering Methods

DOI

2017

Register automata with linear arithmetic

Yu-Fang Chen, Ondřej Lengál, Tony Tan, Zhilin Wu

Logic in Computer Science

DOI

2017

Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints

Zhaowei Xu, Taolue Chen, Zhilin Wu

CADE

DOI

2016

Semipositivity in Separation Logic with Two Variables

Zhilin Wu

International Symposium on Software Engineering: Theories, Tools, and Applications

DOI

2016

A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints

Xincai Gu, Taolue Chen, Zhilin Wu

International Joint Conference on Automated Reasoning

DOI

2016

Verifying Pushdown Multi-Agent Systems against Strategy Logics

Taolue Chen, Fu Song, Zhilin Wu

International Joint Conference on Artificial Intelligence

2016

On temporal logics with data variable quantifications: Decidability and complexity

Fu Song, Zhilin Wu

Information and Computation

DOI

2016

Formal Reasoning on Infinite Data Values: An Ongoing Quest

Taolue Chen, Fu Song, Zhilin Wu

International School on Engineering Trustworthy Software Systems

DOI

2016

The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach

Yu-Fang Chen, Lei Song, Zhilin Wu

International Conference on Computer Aided Verification

DOI

2016

Global Model Checking on Pushdown Multi-Agent Systems

Taolue Chen, Fu Song, Zhilin Wu

AAAI Conference on Artificial Intelligence

DOI

2015

On the Satisfiability of Indexed Linear Temporal Logics

Taolue Chen, Fu Song, Zhilin Wu

International Conference on Concurrency Theory

DOI

2015

On Automated Lemma Generation for Separation Logic with Inductive Definitions

C. Enea, M. Sighireanu, Zhilin Wu

Automated Technology for Verification and Analysis

DOI

2015

Automating Program Proofs Based on Separation Logic with Inductive Definitions

C. Enea, M. Sighireanu, Zhilin Wu

2014

Extending Temporal Logics with Data Variable Quantifications

Fu Song, Zhilin Wu

Foundations of Software Technology and Theoretical Computer Science

DOI

2014

Regular path queries on graphs with data: A rigid approach

Zhilin Wu

arXiv.org

2014

On effective construction of the greatest solution of language inequality XA ⊆ BX

O. Ly, Zhilin Wu

Theoretical Computer Science

DOI

2012

Roles of vegetation, flow type and filled depth on livestock wastewater treatment through multi-level mineralized refuse-based constructed wetlands

Donglin Zhu, Cheng Sun, Houhu Zhang, Zhilin Wu, Bo Jia, Yi Zhang

Ecological Engineering，Vol. 39

DOI

2012

On Injective Embeddings of Tree Patterns

Jakub Michaliszyn, A. Muscholl, S. Staworko, Piotr Wieczorek, Zhilin Wu

arXiv.org

2012

Commutative Data Automata

Zhilin Wu

Annual Conference for Computer Science Logic

DOI

2011

A Decidable Extension of Data Automata

Zhilin Wu

International Symposium on Games, Automata, Logics and Formal Verification

DOI

2010

Verifying Recursive Active Documents with Positive Data Tree Rewriting

B. Genest, A. Muscholl, Zhilin Wu

Foundations of Software Technology and Theoretical Computer Science

DOI

2010

Distributed tree decomposition of graphs and applications to verification

S. Grumbach, Zhilin Wu

IEEE International Symposium on Parallel & Distributed Processing, Workshops and Phd Forum

DOI

2010

An Eﬀective Solution of Language Inequality XA ⊆ BX In the Case of Codes with Finite Decoding Delay

O. Ly, Zhilin Wu

2009

On the distributed evaluation of recursive queries over graphs

S. Grumbach, Fang Wang, Zhilin Wu

arXiv.org

2009

Netquest: An Abstract Model for Pervasive Applications

Michel Bauderon, Christophe Bobineau, S. Grumbach, Antoine Henry, Xin Qi, Wen-Wu Qu, Kun Suo, Fang Wang, Zhilin Wu

International Conference on Pervasive Computing

2009

Feasibility of motion planning on acyclic and strongly connected directed graphs

Zhilin Wu, S. Grumbach

Discrete Applied Mathematics

DOI

2009

On Distributed Model Checking of MSO on Graphs

S. Grumbach, Zhilin Wu

arXiv.org

2009

Logical Locality Entails Frugal Distributed Computation over Graphs (Extended Abstract)

S. Grumbach, Zhilin Wu

International Workshop on Graph-Theoretic Concepts in Computer Science

DOI

2009

Feasibility of Motion Planning on Directed Graphs

Zhilin Wu, S. Grumbach

Theory and Applications of Models of Computation

DOI

2007

A note on the characterization of TL[EF]

Zhilin Wu

Information Processing Letters

DOI

2007

On the Expressive Power of QLTL

Zhilin Wu

International Colloquium on Theoretical Aspects of Computing

DOI

2007

the complexity of dual models problem of propositional linear temporal logics

Zhilin Wu, Wenhui Zhang

DOI

2005

Quasi-star-free Languages on Infinite Words

Zhilin Wu

Acta Cybernetica

2001

Automata theory and its applications

Zhilin Wu, P. Bourhis

DOI

精选作品

期刊论文

A Formally Verified Procedure for Width Inference in FIRRTL

χ RVFormal: Formal verification of RISC-V processor Chisel designs

Can LLM Aid in Solving Constraints with Inductive Definitions?

Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction

An efficient string solver for string constraints with regex-counting and string-length

Separation Logic with Heap Variables: A Decision Procedure and Its Application

OSTRICH2: Solver for Complex String Constraints

Decision Procedure for A Theory of String Sequences

BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions

Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once

Verifying Randomized Consensus Protocols with Common Coins

Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks

SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits

Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps

Formal Verification of RISC-V Processor Chisel Designs

基础设施投资能促进共同富裕吗

A decision procedure for string constraints with string/integer conversion and flat regular constraints

OSTRICH Version 1.3

String Constraints with Regex-Counting and String-Length Solved More Efficiently

The OSTRICH String Solver

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper)

Solving Not-Substring Constraint withFlat Abstraction

Solving string constraints with Regex-dependent functions through transducers with priorities and variables

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata

Monadic Decomposition in Integer Linear Arithmetic

Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps

SL-COMP: Competition of Solvers for Separation Logic

Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints

Android Stack Machine

Decision procedures for path feasibility of string-manipulating programs with complex operations

OSTRICH String Constraint Solver and Results

Review of Equity Risk Premium Puzzle

What is decidable about string constraints with the ReplaceAll function

Tractability of Separation Logic with Inductive Definitions: Beyond Lists

The Complexity of SORE-definability Problems

Model Checking Pushdown Epistemic Game Structures

Register automata with linear arithmetic

Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints

Semipositivity in Separation Logic with Two Variables

A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints

Verifying Pushdown Multi-Agent Systems against Strategy Logics

On temporal logics with data variable quantifications: Decidability and complexity

Formal Reasoning on Infinite Data Values: An Ongoing Quest

The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach

Global Model Checking on Pushdown Multi-Agent Systems

On the Satisfiability of Indexed Linear Temporal Logics

On Automated Lemma Generation for Separation Logic with Inductive Definitions

Automating Program Proofs Based on Separation Logic with Inductive Definitions

Extending Temporal Logics with Data Variable Quantifications

Regular path queries on graphs with data: A rigid approach

On effective construction of the greatest solution of language inequality XA ⊆ BX

Roles of vegetation, flow type and filled depth on livestock wastewater treatment through multi-level mineralized refuse-based constructed wetlands

On Injective Embeddings of Tree Patterns

Commutative Data Automata

A Decidable Extension of Data Automata

Verifying Recursive Active Documents with Positive Data Tree Rewriting

Distributed tree decomposition of graphs and applications to verification

An Eﬀective Solution of Language Inequality XA ⊆ BX In the Case of Codes with Finite Decoding Delay

On the distributed evaluation of recursive queries over graphs

Netquest: An Abstract Model for Pervasive Applications

Feasibility of motion planning on acyclic and strongly connected directed graphs

On Distributed Model Checking of MSO on Graphs

Logical Locality Entails Frugal Distributed Computation over Graphs (Extended Abstract)

Feasibility of Motion Planning on Directed Graphs

A note on the characterization of TL[EF]

On the Expressive Power of QLTL

the complexity of dual models problem of propositional linear temporal logics

Quasi-star-free Languages on Infinite Words

Automata theory and its applications