An Interface Theory Based Approach to Verification of Web Services. - Zhenbang Chen 001; Ji Wang 001; Wei Dong 006; Zhichang Qi; Wing Lok Yeung (COMPSAC (2), 2006)

Towards Formal Interfaces for Web Services with Transactions. - Zhenbang Chen 001; Ji Wang 001; Wei Dong 006; Zhichang Qi (SITIS, 2006)

A Contract-based Approach to Specifying and Verifying Safety Critical Systems. - Wei Dong 006; Zhenbang Chen 001; Ji Wang 001 (FESCA@ETAPS, 2006)

Interface theory-based formalisation and verification of orchestration in BPEL4WS. - Zhenbang Chen 001; Ji Wang 001; Wei Dong 006; Zhichang Qi (Int. J. Bus. Process. Integr. Manag., 2007)

Failure-Divergence Refinement of Compensating Communicating Processes. - Zhenbang Chen 001; Zhiming Liu 001; Ji Wang 001 (FM, 2011)

Topology-Aware Deployment of Scientific Applications in Cloud Computing. - Pei Fan; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Michael R. Lyu (IEEE CLOUD, 2012)

Online Optimization of VM Deployment in IaaS Cloud. - Pei Fan; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng (ICPADS, 2012)

Speculative Symbolic Execution. - Yufeng Zhang 001; Zhenbang Chen 001; Ji Wang 001 (ISSRE, 2012)

A spectral clustering-based optimal deployment method for scientific application in cloud computing. - Pei Fan; Ji Wang 001; Zhenbang Chen 001; Zibin Zheng; Michael R. Lyu (Int. J. Web Grid Serv., 2012)

S2PF: speculative symbolic PathFinder. - Yufeng Zhang 001; Zhenbang Chen 001; Ji Wang 001 (ACM SIGSOFT Softw. Eng. Notes, 2012)

Failure-divergence semantics and refinement of long running transactions. - Zhenbang Chen 001; Zhiming Liu 001; Ji Wang 001 (Theor. Comput. Sci., 2012)

An Operational Semantics for Model Checking Long Running Transactions. - Hengbiao Yu; Zhenbang Chen 001; Ji Wang 001 (WS-FM, 2013)

Towards an Open Data Set for Trace-Oriented Monitoring. - Jingwen Zhou; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Michael R. Lyu (IEEE CLOUD, 2014)

Synchronization Error Detection of MPI Programs by Symbolic Execution. - Xianjin Fu; Zhenbang Chen 001; Chun Huang 006; Wei Dong 006; Ji Wang 001 (APSEC (1), 2014)

Trace Bench: An Open Data Set for Trace-Oriented Monitoring. - Jingwen Zhou; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Michael R. Lyu (CloudCom, 2014)

A Runtime Verification Based Trace-Oriented Monitoring Framework for Cloud Systems. - Jingwen Zhou; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Wei Dong 006 (ISSRE Workshops, 2014)

MTracer: A Trace-Oriented Monitoring Framework for Medium-Scale Distributed Systems. - Jingwen Zhou; Zhenbang Chen 001; Haibo Mi; Ji Wang 001 (SOSE, 2014)

A Predictive Runtime Verification Framework for Cyber-Physical Systems. - Kang Yu; Zhenbang Chen 001; Wei Dong 006 (SERE (Companion), 2014)

MPISE: Symbolic Execution of MPI Programs. - Xianjin Fu; Zhenbang Chen 001; Yufeng Zhang 001; Chun Huang 006; Ji Wang 001 (CoRR, 2014)

A topology-aware method for scientific application deployment on cloud. - Pei Fan; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Michael R. Lyu (Int. J. Web Grid Serv., 2014)

MPISE: Symbolic Execution of MPI Programs. - Xianjin Fu; Zhenbang Chen 001; Yufeng Zhang 001; Chun Huang 006; Wei Dong 006; Ji Wang 001 (HASE, 2015)

Poster: Symbolic Execution of MPI Programs. - Xianjin Fu; Zhenbang Chen 001; Hengbiao Yu; Chun Huang 006; Wei Dong 006; Ji Wang 001 (ICSE (2), 2015)

Regular Property Guided Dynamic Symbolic Execution. - Yufeng Zhang 001; Zhenbang Chen 001; Ji Wang 001; Wei Dong 006; Zhiming Liu 001 (ICSE (1), 2015)

Poster: Segmentation Based Online Performance Problem Diagnosis. - Jingwen Zhou; Zhenbang Chen 001; Ji Wang 001 (ICSE (2), 2015)

RGSE: a regular property guided symbolic executor for Java. - Hengbiao Yu; Zhenbang Chen 001; Yufeng Zhang 001; Ji Wang 001; Wei Dong 006 (ESEC/SIGSOFT FSE, 2017)

MC/DC coverage-oriented compiler optimization for symbolic execution. - Yijun Liu; Zhenbang Chen 001; Wei Dong 006; Chendong Feng (ICSE (Companion Volume), 2018)

Symbolic verification of regular properties. - Hengbiao Yu; Zhenbang Chen 001; Ji Wang 001; Zhendong Su 001; Wei Dong 006 (ICSE, 2018)

Combining Symbolic Execution and Model Checking to Verify MPI Programs. - Hengbiao Yu; Zhenbang Chen 001; Xianjin Fu; Ji Wang 001; Zhendong Su 001; Wei Dong 006; Chun Huang 006 (CoRR, 2018)

Boosting the Robustness Verification of DNN by Identifying the Achilles's Heel. - Chengdong Feng; Zhenbang Chen 001; Weijiang Hong; Hengbiao Yu; Wei Dong 006; Ji Wang 001 (CoRR, 2018)

A Data Set for User Request Trace-Oriented Monitoring and its Applications. - Jingwen Zhou; Zhenbang Chen 001; Ji Wang 001; Zibin Zheng; Michael R. Lyu (IEEE Trans. Serv. Comput., 2018)

Evaluation of model checkers by verifying message passing programs. - Weijiang Hong; Zhenbang Chen 001; Hengbiao Yu; Ji Wang 001 (Sci. China Inf. Sci., 2019)

Symbolic Verification of Regular Properties for Java Programs. - Zhenbang Chen 001; Hengbiao Yu; Ji Wang 001; Wei Dong 006 (ACM SIGSOFT Softw. Eng. Notes, 2019)

MPI-SV: a symbolic verifier for MPI programs. - Zhenbang Chen 001; Hengbiao Yu; Xianjin Fu; Ji Wang 001 (ICSE (Companion Volume), 2020)

Symbolic verification of message passing interface programs. - Hengbiao Yu; Zhenbang Chen 001; Xianjin Fu; Ji Wang 001; Zhendong Su 001; Jun Sun 001; Chun Huang 006; Wei Dong 006 (ICSE, 2020)

Styx: A Data-Oriented Mutation Framework to Improve the Robustness of DNN. - Meixi Liu; Weijiang Hong; Weiyu Pan; Chendong Feng; Zhenbang Chen 001; Ji Wang 001 (ASE, 2020)

Multiplex Symbolic Execution: Exploring Multiple Paths by Solving Once. - Yufeng Zhang 001; Zhenbang Chen 001; Ziqi Shuai; Tianqi Zhang; Kenli Li 001; Ji Wang 001 (ASE, 2020)

Efficient Multiplex Symbolic Execution with Adaptive Search Strategy. - Tianqi Zhang; Yufeng Zhang 001; Zhenbang Chen 001; Ziqi Shuai; Ji Wang 001 (ASE, 2020)

Symbolic Verification of MPI Programs with Non-deterministic Synchronizations. - Hengbiao Yu; Zhenbang Chen 001; Chun Huang 006; Ji Wang 001 (SETTA, 2020)

Out-of-Distribution Detection with Distance Guarantee in Deep Generative Models. - Yufeng Zhang 001; Wanwei Liu; Zhenbang Chen 001; Ji Wang 001; Zhiming Liu 001; Kenli Li 001; Hongmei Wei; Zuoning Chen (CoRR, 2020)

Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution. - Weijiang Hong; Yijun Liu; Zhenbang Chen 001; Wei Dong 006; Ji Wang 001 (Frontiers Inf. Technol. Electron. Eng., 2020)

The Java Pathfinder Workshop 2019. - Cyrille Artho; Quoc-Sang Phan; Peter Aldous; Alyas Almaawi; Lucas Bang; Lasse Berglund; Tevfik Bultan; Zhenbang Chen 001; Hayes Converse; Wei Dong 006; William Eiers; Milos Gligoric 001; et al. (ACM SIGSOFT Softw. Eng. Notes, 2020)

Trace Abstraction-Based Verification for Uninterpreted Programs. - Weijiang Hong; Zhenbang Chen 001; Yide Du; Ji Wang 001 (FM, 2021)

Synthesize solving strategy for symbolic execution. - Zhenbang Chen 001; Zehua Chen; Ziqi Shuai; Guofeng Zhang 005; Weiyu Pan; Yufeng Zhang 001; Ji Wang 001 (ISSTA, 2021)

Grammar-agnostic symbolic execution by token symbolization. - Weiyu Pan; Zhenbang Chen 001; Guofeng Zhang 005; Yunlai Luo; Yufeng Zhang 001; Ji Wang 001 (ISSTA, 2021)

Type and interval aware array constraint solving for symbolic execution. - Ziqi Shuai; Zhenbang Chen 001; Yufeng Zhang 001; Jun Sun 001; Ji Wang 001 (ISSTA, 2021)

On the Properties of Kullback-Leibler Divergence Between Gaussians. - Yufeng Zhang 001; Wanwei Liu; Zhenbang Chen 001; Kenli Li 001; Ji Wang 001 (CoRR, 2021)

Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization. - Guofeng Zhang 005; Zhenbang Chen 001; Ziqi Shuai; Yufeng Zhang 001; Ji Wang 001 (APSEC, 2022)

Collaborative Verification of Uninterpreted Programs. - Yide Du; Weijiang Hong; Zhenbang Chen 001; Ji Wang 001 (TASE, 2022)

Unsatisfiable Core Based Constraint Solving Cache in Symbolic Execution. - Ziqi Shuai; Zhenbang Chen 001; Yufeng Zhang 001; Hengbiao Yu; Ji Wang 001 (APSEC, 2023)

Symbolic Verification of Fuzzy Logic Models. - Siang Zhao; Zhongyang Li; Zhenbang Chen 001; Ji Wang 001 (ASE, 2023)

On the Properties of Kullback-Leibler Divergence Between Multivariate Gaussian Distributions. - Yufeng Zhang 001; Jialu Pan; Li Ken Li; Wanwei Liu; Zhenbang Chen 001; Xinwang Liu 002; Ji Wang 001 (NeurIPS, 2023)

CSP based Formal Modeling and Verification of Behavior Trees. - Peishan Huang; Weijiang Hong; Zhenbang Chen 001; Ji Wang 001 (QRS Companion, 2023)

CCMOP: A Runtime Verification Tool for C/C++ Programs. - Yongchao Xing; Zhenbang Chen 001; Shibo Xu; Yufeng Zhang 001 (RV, 2023)

Formal Verification Based Synthesis for Behavior Trees. - Weijiang Hong; Zhenbang Chen 001; Minglong Li; Yuhan Li; Peishan Huang; Ji Wang 001 (SETTA, 2023)

Preface to the Special Issue on Constraint Solving and Theorem Proving. - Shaowei Cai 001; Zhenbang Chen 001; Ji Wang 001; Bohua Zhan; Yongwang Zhao (Int. J. Softw. Informatics, 2023)

FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution). - Guofeng Zhang 005; Ziqi Shuai; Kelin Ma; Kunlin Liu; Zhenbang Chen 001; Ji Wang 001 (FASE, 2024)

Hybrid Regression Test Selection by Integrating File and Method Dependences. - Guofeng Zhang 005; Luyao Liu; Zhenbang Chen 001; Ji Wang 001 (ASE, 2024)

Hybrid Regression Test Selection by Synergizing File and Method Call Dependences. - Luyao Liu; Guofeng Zhang 005; Zhenbang Chen 001; Ji Wang 001 (SIGSOFT FSE Companion, 2024)

AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution). - Zhen Wang; Zhenbang Chen 001 (TACAS (3), 2024)

Partial Solution Based Constraint Solving Cache in Symbolic Execution. - Ziqi Shuai; Zhenbang Chen 001; Kelin Ma; Kunlin Liu; Yufeng Zhang 001; Jun Sun 001; Ji Wang 001 (Proc. ACM Softw. Eng., 2024)

Verification of message-passing uninterpreted programs. - Weijiang Hong; Zhenbang Chen 001; Yufeng Zhang 001; Hengbiao Yu; Yide Du; Ji Wang 001 (Sci. Comput. Program., 2024)

Adaptive solving strategy synthesis for symbolic execution. - Zhenbang Chen 001; Guofeng Zhang 005; Zehua Chen; Ziqi Shuai; Weiyu Pan; Yufeng Zhang 001; Ji Wang 001 (J. Softw. Evol. Process., 2024)

Kullback-Leibler Divergence-Based Out-of-Distribution Detection With Flow-Based Generative Models. - Yufeng Zhang 001; Jialu Pan; Wanwei Liu; Zhenbang Chen 001; Kenli Li 001; Ji Wang 001; Zhiming Liu 001; Hongmei Wei (IEEE Trans. Knowl. Data Eng., 2024)

Symbolic Execution Based Automatic Performance Optimization for MPI Programs. - Zheng Bian; Zhenbang Chen 001; Ji Wang 001 (SIGSOFT FSE Companion, 2025)

AISE v2.0: Combining Loop Transformations - (Competition Contribution). - Yao Lin; Zhenbang Chen 001; Ji Wang 001 (TACAS (3), 2025)

Symbolic execution of floating-point programs: How far are we? - Xu Yang; Guofeng Zhang 005; Ziqi Shuai; Zhenbang Chen 001; Ji Wang 001 (J. Syst. Softw., 2025)

Multi-modal Sketch-Based Behavior Tree Synthesis. - Wenmeng Zhang; Zhenbang Chen 001; Weijiang Hong (Proc. ACM Program. Lang., 2025)

QSF: Multi-objective Optimization Based Efficient Solving for Floating-Point Constraints. - Xu Yang; Zhenbang Chen 001; Wei Dong 006; Ji Wang 001 (Proc. ACM Softw. Eng., 2025)

FDSE v2: Variable Importance Guided Hybrid Fuzzing (Competition Contribution). - Guofeng Zhang 005; Zhenbang Chen 001; Ji Wang 001 (FASE, 2026)

EUF-based Solving Dyck-Reachability with Applications to Static Analysis. - Yide Du; Zhenbang Chen 001; Kunlin Liu; Guofeng Zhang 005; Xudong Wang; Ke Ma; Wei Dong 006; Ji Wang 001 (FM (2), 2026)

S2F: Principled Hybrid Testing With Fuzzing, Symbolic Execution, and Sampling. - Lianjing Wang; Yufeng Zhang 001; Kenli Li 001; Zhenbang Chen 001; Xu Zhou 001; Pengfei Wang; Guangning Song; Ji Wang 001 (CoRR, 2026)

Integrating Path Selection for Symbolic Execution and Variable Selection for Constraint Solving. - Shunkai Zhu; Jun Sun 001; Jingyi Wang 004; Zhenbang Chen 001; Peng Cheng 007 (ACM Trans. Softw. Eng. Methodol., 2026)