Posts by Collection

portfolio

. Portfolio item number 1,

Short description of portfolio item number 1

. Portfolio item number 2,

Short description of portfolio item number 2

projects

. 2012 Nsfc,

. 2015 Nsfc,

. 2018 Nsfc,

. 2022 Nsfc,

publications

**Zhenbang Chen**, Ji Wang, Wei Dong, Zhichang Qi. An Interface Model for Service-Oriented Software Architecture (in Chinese),

**Zhenbang Chen**, Ji Wang, Wei Dong, Zhichang Qi, Wing Lok Yeung. An Interface Theory Based Approach to Verification of Web Services,

Wei Dong, **Zhenbang Chen**, Ji Wang. A Contract-based Approach to Specifying, Verifying Safety CriticalSystems,

**Zhenbang Chen**, Ji Wang, Wei Dong, Zhichang Qi. Towards Formal Interfaces for Web Services with Transactions,

**Zhenbang Chen**, Xiaoshan Li, Zhiming Liu, Volker Stolz, Lu Yang. Harnessing rCOS for Tool Support - The CoCoME Experience,

**Zhenbang Chen**, Abdelhakim Hannousse, Dang Van Hung, Istvan Knoll, Xiaoshan Li, Zhiming Liu, Yang Liu, Qu Nan, Joseph C. Okika, Anders P. Ravn, Volker Stolz, Lu Yang, Naijun Zhan. Modelling with Relational Calculus of Object, Component Systems- rCOS,

**Zhenbang Chen**, Zhiming Liu, Volker Stolz, Lu Yang, Anders P. Ravn. A Refinement Driven Component-Based Design,

**Zhenbang Chen**, Ji Wang, Wei Dong, Zhichang Qi. Interface theory-based formalisation, verification of orchestrationin BPEL4WS,

Zuohua Ding, **Zhenbang Chen**, Jing Liu. A Rigorous Model of Service Component Architecture,

**Zhenbang Chen**, Charles Morisset, Volker Stolz. Specification, Validation of Behavioural Protocols in the rCOS Modeler,

**Zhenbang Chen**, Zhiming Liu, Anders P. Ravn, Volker Stolz, Naijun Zhan. Refinement, verification in component-based model-driven design,

**Zhenbang Chen**, Zhiming Liu. An Extended cCSP with Stable Failures Semantics,

Xiang Rao, Huaimin Wang, Dianxi Shi, **Zhenbang Chen**, Hua Cai, Qi Zhou, Tingtao Sun. Identifying faults in large-scale distributed systems by filteringnoisy error logs,

**Zhenbang Chen**, Zhiming Liu, Ji Wang. Failure-Divergence Refinement of Compensating Communicating Processes,

Pei Fan, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Michael R. Lyu. Topology-Aware Deployment of Scientific Applications in Cloud Computing,

Haibo Mi, Huaimin Wang, Hua Cai, Yangfan Zhou, Michael R. Lyu, **Zhenbang Chen**. P-Tracer: Path-Based Performance Profiling in Cloud Computing Systems,

Pei Fan, **Zhenbang Chen**, Ji Wang, Zibin Zheng. Online Optimization of VM Deployment in IaaS Cloud,

Pei Fan, Ji Wang, **Zhenbang Chen**, Zibin Zheng, Michael R. Lyu. A spectral clustering-based optimal deployment method for scientificapplication in cloud computing,

Yufeng Zhang, **Zhenbang Chen**, Ji Wang. Speculative Symbolic Execution,

Yufeng Zhang, **Zhenbang Chen**, Ji Wang. S2PF: speculative symbolic PathFinder,

**Zhenbang Chen**, Zhiming Liu, Ji Wang. Failure-divergence semantics, refinement of long running transactions,

Chengsong Wang, **Zhenbang Chen**, Xiaoguang Mao. Optimizing Nop-shadows Typestate Analysis by Filtering Interferential Configurations,

Hengbiao Yu, **Zhenbang Chen**, Ji Wang. An Operational Semantics for Model Checking Long Running Transactions,

Jingwen Zhou, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Michael R. Lyu. Towards an Open Data Set for Trace-Oriented Monitoring,

Xianjin Fu, **Zhenbang Chen**, Chun Huang, Wei Dong, Ji Wang. Synchronization Error Detection of MPI Programs by Symbolic Execution,

Jingwen Zhou, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Michael R. Lyu. Trace Bench: An Open Data Set for Trace-Oriented Monitoring,

Xianjin Fu, **Zhenbang Chen**, Yufeng Zhang, Chun Huang, Ji Wang. MPISE: Symbolic Execution of MPI Programs,

Pei Fan, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Michael R. Lyu. A topology-aware method for scientific application deployment on cloud,

Jingwen Zhou, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Wei Dong. A Runtime Verification Based Trace-Oriented Monitoring Framework for Cloud Systems,

Haibo Mi, Huaimin Wang, **Zhenbang Chen**, Yangfan Zhou. Automatic Detecting Performance Bugs in Cloud Computing Systems viaLearning Latency Specification Model,

Jingwen Zhou, **Zhenbang Chen**, Haibo Mi, Ji Wang. MTracer: A Trace-Oriented Monitoring Framework for Medium-ScaleDistributed Systems,

Kang Yu, **Zhenbang Chen**, Wei Dong. A Predictive Runtime Verification Framework for Cyber-Physical Systems,

Xianjin Fu, **Zhenbang Chen**, Yufeng Zhang, Chun Huang, Wei Dong, Ji Wang. MPISE: Symbolic Execution of MPI Programs,

Xianjin Fu, **Zhenbang Chen**, Hengbiao Yu, Chun Huang, Wei Dong, Ji Wang. Poster: Symbolic Execution of MPI Programs,

Yufeng Zhang, **Zhenbang Chen**, Ji Wang, Wei Dong, Zhiming Liu. Regular Property Guided Dynamic Symbolic Execution,

Jingwen Zhou, **Zhenbang Chen**, Ji Wang. Poster: Segmentation Based Online Performance Problem Diagnosis,

Hengbiao Yu, **Zhenbang Chen**, Yufeng Zhang, Ji Wang, Wei Dong. RGSE: a regular property guided symbolic executor for Java,

Hengbiao Yu, **Zhenbang Chen**, Xianjin Fu, Ji Wang, Zhendong Su, Wei Dong, Chun Huang. Combining Symbolic Execution and Model Checking to Verify MPI Programs,

Chengdong Feng, **Zhenbang Chen**, Weijiang Hong, Hengbiao Yu, Wei Dong, Ji Wang. Boosting the Robustness Verification of DNN by Identifying the Achilles'sHeel,

Yijun Liu, **Zhenbang Chen**, Wei Dong, Chendong Feng. MC/DC coverage-oriented compiler optimization for symbolic execution,

Xinyu Wang, Jun Sun, **Zhenbang Chen**, Peixin Zhang, Jingyi Wang, Yun Lin. Towards optimal concolic testing,

Hengbiao Yu, **Zhenbang Chen**, Ji Wang, Zhendong Su, Wei Dong. Symbolic verification of regular properties,

Jingwen Zhou, **Zhenbang Chen**, Ji Wang, Zibin Zheng, Michael R. Lyu. A Data Set for User Request Trace-Oriented Monitoring, its Applications,

Weijiang Hong, **Zhenbang Chen**, Hengbiao Yu, Ji Wang. Evaluation of model checkers by verifying message passing programs,

Jian Zhang, Chao Zhang, Jifeng Xuan, Yingfei Xiong, Qianxiang Wang, Bin Liang, Lian Li, Wensheng Dou, **Zhenbang Chen**, Liqian Chen, Yan Cai. Recent Progress in Program Analysis (in Chinese),

**Zhenbang Chen**, Hengbiao Yu, Ji Wang, Wei Dong. Symbolic Verification of Regular Properties for Java Programs,

Yufeng Zhang, Wanwei Liu, **Zhenbang Chen**, Ji Wang, Zhiming Liu, Kenli Li, Hongmei Wei, Zuoning Chen. Out-of-Distribution Detection with Distance Guarantee in Deep GenerativeModels,

**Zhenbang Chen**, Hengbiao Yu, Xianjin Fu, Ji Wang. MPI-SV: A Symbolic Verifier for MPI Programs,

Hengbiao Yu, **Zhenbang Chen**, Xianjin Fu, Ji Wang, Zhendong Su, Jun Sun, Chun Huang, Wei Dong. Symbolic verification of message passing interface programs,

Weijiang Hong, Yijun Liu, **Zhenbang Chen**, Wei Dong, Ji Wang. Modified condition/decision coverage (MC/DC) oriented compiler optimizationfor symbolic execution,

Zehua Chen, **Zhenbang Chen**, Ziqi Shuai, Yufeng Zhang, Weiyu Pan. Synthesizing Smart Solving Strategy for Symbolic Execution,

Meixi Liu, Weijiang Hong, Weiyu Pan, Chendong Feng, **Zhenbang Chen**, Ji Wang. Styx: A Data-Oriented Mutation Framework to Improve the Robustnessof DNN,

Yufeng Zhang, **Zhenbang Chen**, Ziqi Shuai, Tianqi Zhang, Kenli Li, Ji Wang. Multiplex Symbolic Execution: Exploring Multiple Paths by Solving Once,

Tianqi Zhang, Yufeng Zhang, **Zhenbang Chen**, Ziqi Shuai, Ji Wang. Efficient Multiplex Symbolic Execution with Adaptive Search Strategy,

Hengbiao Yu, **Zhenbang Chen**, Chun Huang, Ji Wang. Symbolic Verification of MPI Programs with Non-deterministic Synchronizations,

Yufeng Zhang, Wanwei Liu, **Zhenbang Chen**, Kenli Li, Ji Wang. On the Properties of Kullback-Leibler Divergence Between Gaussians,

Weijiang Hong, **Zhenbang Chen**, Yide Du, Ji Wang. Trace Abstraction-Based Verification for Uninterpreted Programs,

Jinjian Luo, Meixi Liu, Yunlai Luo, **Zhenbang Chen**, Yufeng Zhang. A Runtime Monitoring Based Fuzzing Framework for Temporal Properties,

**Zhenbang Chen**, Zehua Chen, Ziqi Shuai, Guofeng Zhang, Weiyu Pan, Yufeng Zhang, Ji Wang. Synthesize solving strategy for symbolic execution,

Weiyu Pan, **Zhenbang Chen**, Guofeng Zhang, Yunlai Luo, Yufeng Zhang, Ji Wang. Grammar-agnostic symbolic execution by token symbolization,

Ziqi Shuai, **Zhenbang Chen**, Yufeng Zhang, Jun Sun, Ji Wang. Type and interval aware array constraint solving for symbolic execution,

Yang Liu, Guofeng Zhang, **Zhenbang Chen**, Ziqi Shuai. Selective Symbolization Based Efficient Symbolic Execution,

Guofeng Zhang, **Zhenbang Chen**, Ziqi Shuai. Symbolic Execution of Floating-point Programs: How far are we?,

Guofeng Zhang, **Zhenbang Chen**, Ziqi Shuai, Yufeng Zhang, Ji Wang. Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization,

Yide Du, Weijiang Hong, **Zhenbang Chen**, Ji Wang. Collaborative Verification of Uninterpreted Programs,

Siang Zhao, Zhongyang Li, **Zhenbang Chen**, Ji Wang. Symbolic Verification of Fuzzy Logic Models,

Nenghui Hu, Zheng Bian, Ziqi Shuai, **Zhenbang Chen**, Yufeng Zhang. Symbolic Execution of MPI Programs with One-Sided Communications,

Ziqi Shuai, **Zhenbang Chen**, Yufeng Zhang, Yufeng Zhang, Hengbiao Yu, Ji Wang. Unsatisfiable Core Based Constraint Solving Cache in Symbolic Execution,

Yide Du, Weijiang Hong, **Zhenbang Chen**, Ji Wang. Collaborative Verification of Uninterpreted Programs (in Chinese),

**Zhenbang Chen**, Guofeng Zhang, Zehua Chen, Ziqi Shuai, Weiyu Pan, Yufeng Zhang, Ji Wang. Adaptive solving strategy synthesis for symbolic execution,

Yufeng Zhang, Jialu Pan, Kenli Li, Wanwei Liu, **Zhenbang Chen**, Xinwang Liu, Ji Wang. On the Properties of Kullback-Leibler Divergence Between Multivariate Gaussian Distributions,

Yongchao Xing, **Zhenbang Chen**, Shibo Xu, Yufeng Zhang. CCMOP: A Runtime Verification Tool for C/C++ Programs,

Hengbiao Yu, Xin Yi, Banghu Yin, Fa Li, **Zhenbang Chen**, Chun Huang. Efficient Generation of Floating-Point Inputs for Compiler-Induced Variability,

Weijiang Hong, **Zhenbang Chen**, Minglong Li, Yuhan Li, Peishan Huang, Ji Wang. Formal Verification based Synthesis for Behavior Trees,

Yufeng Zhang, Jialu Pan, Wanwei Liu, **Zhenbang Chen**, Kenli Li, Ji Wang, Zhiming Liu, Hongmei Wei. Kullback-Leibler Divergence-Based Out-of-Distribution Detection with Flow-Based Generative Models,

Guofeng Zhang, Luyao Liu, **Zhenbang Chen**, Ji Wang. Hybrid Regression Test Selection by Integrating File and Method Dependences,

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

Ziqi Shuai, **Zhenbang Chen**, Kelin Ma, Kunlin Liu, Yufeng Zhang, Jun Sun, Ji Wang. Partial Solution Based Constraint Solving Cache in Symbolic Execution,

Luyao Liu, Guofeng Zhang, **Zhenbang Chen**, Ji Wang. Hybrid Regression Test Selection by Synergizing File and Method Call Dependences.,

Xu Yang, Guofeng Zhang, Ziqi Shuai, **Zhenbang Chen**, Ji Wang. Symbolic Execution of Floating-point Programs: How far are we?,

Weijiang Hong, **Zhenbang Chen**, Yufeng Zhang, Henbiao Yu, Yide Du, Ji Wang. Verification of Message-passing Uninterpreted Programs,

Zheng Wang, **Zhenbang Chen**. AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution),

Xu Yang, **Zhenbang Chen**, Wei Dong, Ji Wang. QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints,

Zheng Bian, **Zhenbang Chen**, Ji Wang. Symbolic Execution Based Automatic Performance Optimization for MPI Programs,

Wenmeng Zhang, **Zhenbang Chen**, Weijiang Hong. Multi-Modal Sketch-based Behavior Tree Synthesis,

Yao Lin, **Zhenbang Chen**, Ji Wang. AISE v2.0: Combining Loop Transformations (Competition Contribution),

Shunkai Zhu, Jun Sun, Jingyi Wang, **Zhenbang Chen**, Peng Cheng. Path Selection for Symbolic Execution and Variable Selection for Constraint Solving,

services

. Acmcs,

. Ai Testing,

. Ase,

. Ese,

. Facs,

. Fcs,

. Fmac,

. Formalise,

. Icfem,

. Ictac,

. Issta,

. Ist,

. Internetware,

. Jcst,

. Jisa,

. Jlamp,

. Jos,

. Jss,

. Models,

. Nasac,

. Saner,

. Sate,

. Scis,

. Scp,

. Sefm,

. Sqj,

. Tase,

. Tr,

. Tse,

. Vecos,

. Yr Fmac,

. Yr Setta,

students

. 2008 Fp,

. 2009 Zyf,

. 2010 Fxj,

. 2011 Zjw,

. 2015 Lyj,

. 2015 Jww,

. 2014 Yhb,

. 2017 Fcd,

. 2017 Hwj,

. 2018 Czh,

. 2018 Ljj,

. 2018 Ztq,

. 2019 Dyd,

. 2019 Ly,

. 2019 Pwy,

. 2022 Lkl 1,

. 2022 Lzy,

. 2022 Mkl 1,

. 2023 Wd,

. 2019 Lmx,

. 2020 Zgf,

. 2019 Szq,

. 2020 Lyl,

. 2023 By,

. 2023 Hj,

. 2023 Hzr 1,

. 2023 Xsb,

. 2020 Hnh,

. 2020 Zsa,

. 2021 Hps,

. 2020 Hwj,

. 2021 Lly,

. 2021 Wz,

. 2021 Xyc,

. 2024 Chk,

. 2024 Cmh,

. 2022 Bz,

. 2022 Mkl,

. 2025 Cys,

. 2025 Djq,

. 2025 Wq,

. 2023 Hzr,

. 2023 Ly,

. 2023 Yjq,

. 2022 Lkl,

. 2022 Yx,

. 2024 Cmh 1,

. 2024 Dml,

. 2023 Lmx,

. 2023 Mk,

. 2023 Zgf,

. 2023 Wxd,

. 2023 Zwm,

. 2024 Dyd,

. 2024 Hps,

. 2024 Lh,

. 2024 Tx,

. 2024 Wl,

. 2024 Zpy,

. 2025 Wz,

. 2025 Yjq,

talks

. An Extended cCSP with Stable Failures Semantics,

. Failure-Divergence Refinement of Compensating Communicating Processes,

. An Operational Semantics for Model Checking Long Running Transactions,

. Synchronization Error Detection of MPI Programs by Symbolic Execution,

. Regular Property Guided Dynamic Symbolic Execution,

. Symbolic verification of regular properties,

. Symbolic verification of message passing interface programs,

. Synthesize solving strategy for symbolic execution,

. Grammar-agnostic symbolic execution by token symbolization,

. Type and interval aware array constraint solving for symbolic execution,

. Symbolic execution: progress and challenges,

. Symbolic execution oriented constraint solving,

. Partial Solution Based Constraint Solving Cache in Symbolic Execution,

. Symbolic execution: progress and challenges,

. QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints,

teaching

. Computer Programming,

. Computer Basis,

. Computer Programming,

. Software Reliability and Testing,

. Software Qulity Assurance,

. Computer Programming,

. Software Reliability and Testing,

. Software Qulity Assurance,