| 2026 | TASE | PAT2PRISM: Bridging Qualitative Correctness and Quantitative Resilience for IoT Protocols. | Zihan Tang, Sini Chen, Lili Xiao, Huibiao Zhu |
| 2025 | APSEC | BDafny: A Formal Execution and Verification Framework of BPMN 2.0 in Dafny. | Ziqing Su, Sini Chen, Ran Li, Huibiao Zhu, Jiapeng Wang |
| 2025 | ICPADS | NL2CSP: Towards Automated CSP Code Generation with Large Language Models. | Chenhui Wang, Nuowei Liu, Han Bao, Di Wu, Huiying Liu, Jiaqi Yin, Huibiao Zhu |
| 2025 | QRS | A Framework for Verifying BPMN with Hoare Logic. | Wei Lin, Sini Chen, Huibiao Zhu |
| 2025 | SEKE | Verifying the Communication and Security Mechanisms of WAMP. | Han Bao, Chenhui Wang, Huibiao Zhu |
| 2025 | SEKE | Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types (S). | Huiying Liu, Huibiao Zhu, Sini Chen |
| 2025 | SEKE | Formalization and Verification of XMPP Communication Mechanism Using CSP (S). | Di Wu, Wenting Dong, Huibiao Zhu |
| 2024 | COMPSAC | Formal Verification and Security Analysis of AMQP. | Huiying Liu, Wenting Dong, Huibiao Zhu, Ziqing Su |
| 2024 | COMPSAC | Trace and Algebraic Semantics for Partial Store Order Memory Model. | Junfu Luo, Lili Xiao, Huibiao Zhu, Ziqing Su |
| 2024 | COMPSAC | Formalization and Verification of OpenStack Swift Using CSP. | Ziqing Su, Wei Lin, Huibiao Zhu |
| 2024 | COMPSAC | Formalization and Verification of Percolator Using CSP. | Chenhui Wang, Ziqing Su, Huibiao Zhu |
| 2024 | ICTAC | Formal Foundations for Efficient Simulation of MOM Systems: The Refinement Calculus for Object-Oriented Event-Graphs. | Sini Chen, Huibiao Zhu, Ran Li, Lili Xiao, Jiapeng Wang, Ning Ge, Xinbin Cao |
| 2024 | ISSRE | A Security Verification Framework for the LoRaWAN Protocol with Application in the Manufacturing Industry. | Wenting Dong, Huibiao Zhu, Sini Chen, Ning Ge |
| 2024 | SAC | Formalization and Verification of Delegate Contract Signing Mechanism Based on Smart Contract Using CSP. | Bangjie Zhu, Jiaqi Yin, Sini Chen, Huibiao Zhu |
| 2024 | SEKE | Modeling and Verifying OPC UA of Aggregating Server Architecture for Vertical Integration. | Zifan Liang, Wei Lin, Sini Chen, Huibiao Zhu |
| 2024 | SEKE | Validating Secure Cloud Communication Mechanisms of Graphene with CSP-based Modeling. | Jianhao Liu, Zhiru Hou, Huibiao Zhu |
| 2024 | SEKE | Formalization and Verification of the Message Delivery Mechanism of Apache Pulsar. | Wenbin Wu, Zhiru Hou, Huibiao Zhu |
| 2023 | APSEC | Formalization and Verification of Go-based New Simple Queue System. | Danyang Wang, Jiaqi Yin, Sini Chen, Huibiao Zhu |
| 2023 | ISSRE | Formalization and Verification of the ICC Mechanism in Android System Using CSP. | Yixiao Lv, Jiaqi Yin, Sini Chen, Huibiao Zhu |
| 2023 | SEKE | Formalization and Verification of Data Auction Mechanism Based on Smart Contract Using CSP. | Yingjia Du, Yuan Fei, Sini Chen, Huibiao Zhu |
| 2022 | COMPSAC | Formal Analysis and Verification of DPSTM v2 Architecture Using CSP. | Peimu Li, Jiaqi Yin, Huibiao Zhu, Lili Xiao, Miroslav Popovic |
| 2022 | COMPSAC | Algebraic Semantics for C++11 Memory Model. | Lili Xiao, Huibiao Zhu, Mengda He, Shengchao Qin |
| 2022 | ICECCS | Denotational and Algebraic Semantics for Cyber-physical Systems. | Ran Li, Huibiao Zhu, Richard Banach |
| 2022 | ICECCS | The Operational and Denotational Semantics of rMECal Calculus for Mobile Edge Computing. | Jiaqi Yin, Huibiao Zhu |
| 2022 | ICFEM | A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency. | Ran Li, Huibiao Zhu, Richard Banach |
| 2022 | ICTAC | Denotational and Algebraic Semantics for the CaIT Calculus. | Ningning Chen, Huibiao Zhu |
| 2022 | PDCAT | Formalization and Verification of SIP Using CSP. | Zhiru Hou, Jiaqi Yin, Huibiao Zhu, Ningning Chen |
| 2022 | PDCAT | MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. | Junfu Luo, Jiaqi Yin, Huibiao Zhu |
| 2022 | SEKE | Formal Verification of COCO Database Framework Using CSP. | Peimu Li, Jiaqi Yin, Huibiao Zhu |
| 2022 | SEKE | Modeling and Verifying AUPS Using CSP. | Hongqin Zhang, Huibiao Zhu, Jiaqi Yin, Ningning Chen |
| 2022 | SETTA | Translating CPS with Shared-Variable Concurrency in SpaceEx. | Ran Li, Huibiao Zhu, Richard Banach |
| 2021 | DATE | SC4MEC: Automated Implementation of A Secure Hierarchical Calculus for Mobile Edge Computing. | Jiaqi Yin, Huibiao Zhu, Yuan Fei |
| 2021 | ISPA | Modeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP. | Chen Zhao, Jiaqi Yin, Huibiao Zhu, Ran Li |
| 2021 | PDCAT | Formalization and Verification of Group Communication CoAP Using CSP. | Sini Chen, Ran Li, Huibiao Zhu |
| 2021 | TrustCom | Formal Verification of HPS-based Master-Slave Scheme in MEC with Timed Automata. | Jiaqi Yin, Huibiao Zhu, Yuan Fei |
| 2021 | SEKE | Formalization and Verification of Dubbo Using CSP. | Zhiru Hou, Jiaqi Yin, Huibiao Zhu |
| 2021 | SEKE | Formal Modeling and Verification of ICN-IoT Middleware Architecture (S). | Hongqin Zhang, Jiaqi Yin, Huibiao Zhu, Ningning Chen |
| 2021 | SETTA | Trace Semantics and Algebraic Laws for MCA ARMv8 Architecture Based on UTP. | Lili Xiao, Huibiao Zhu |
| 2021 | TASE | A Proof System for HRML with Extended Hoare Logic. | Ningning Chen, Huibiao Zhu, Huixing Fang |
| 2021 | TASE | Formal Modelling and Verification of the RTPS Behavior Module. | Jiaqi Yin, Huibiao Zhu, Yuan Fei, Qiwen Xu |
| 2020 | APSEC | Modeling and Verifying Data Access Mechanism of NLSR Trust Model. | Ningning Chen, Huibiao Zhu, Yuan Fei, Lili Xiao, Jiaqi Yin |
| 2020 | TrustCom | Modeling and Analysis of RabbitMQ Using UPPAAL. | Ran Li, Jiaqi Yin, Huibiao Zhu |
| 2020 | SEKE | Formalization and Verification of VANET. | Ran Li, Huibiao Zhu, Lili Xiao, Jiaqi Yin, Yuan Fei, Gang Lu |
| 2020 | SEKE | Formal Modelling and Verification of MCAC Router Architecture in ICN. | Junya Xu, Huibiao Zhu, Lili Xiao, Jiaqi Yin, Yuan Fei, Gang Lu |
| 2020 | SEKE | Modeling and Verifying NDN-based IoV Using CSP. | Ningning Chen, Huibiao Zhu, Jiaqi Yin, Lili Xiao, Yuan Fei |
| 2020 | TASE | An Axiomatic Approach to BigrTiMo. | Wanling Xie, Huibiao Zhu, Shengchao Qin |
| 2019 | APSEC | Towards the Mechanized Semantics and Refinement of UML Class Diagrams. | Feng Sheng, Huibiao Zhu, Zongyuan Yang |
| 2019 | ICFEM | A Security Calculus for Wireless Networks of Named Data Networking. | Yuan Fei, Huibiao Zhu, Haiying Sun, Jiaqi Yin |
| 2019 | ICFEM | PDNet: A Programming Language for Software-Defined Networks with VLAN. | Shuangqing Xiang, Marcello M. Bonsangue, Huibiao Zhu |
| 2019 | SEKE | Verifying Static Aspects of UML models using Prolog (S). | Feng Sheng, Huibiao Zhu, Zongyuan Yang, Jiaqi Yin, Gang Lu |
| 2019 | SEKE | Modeling and Verifying TESAC Using CSP. | Dongzhen Sun, Huibiao Zhu, Yuan Fei, Lili Xiao, Gang Lu, Jiaqi Yin |
| 2019 | SEKE | Formalization and Verification of RTPS StatefulWriter Module Using CSP. | Jiaqi Yin, Huibiao Zhu, Yuan Fei, Qiwen Xu, Ruobiao Wu |
| 2019 | TASE | Verifying Opacity of a Modified PSTM. | Yucheng Fang, Huibiao Zhu, Jiaqi Yin |
| 2019 | TASE | Modeling and Verifying Transaction Scheduling for Software Transactional Memory using CSP. | Chao Xu, Xi Wu, Huibiao Zhu, Miroslav Popovic |
| 2019 | TASE | A Logical Approach for the Schedulability Analysis of CCSL. | Yuanrui Zhang, Frdric Mallet, Huibiao Zhu, Yixiang Chen |
| 2018 | COMPSAC | Modeling and Verifying MooseFS in CSP. | Yucheng Fang, Huibiao Zhu, Gang Lu, Lili Xiao, Wanling Xie |
| 2018 | COMPSAC | Modeling and Verifying OpenFlow Scheduled Bundle Mechanism Using CSP. | Huiwen Wang, Huibiao Zhu, Lili Xiao, Wanling Xie, Gang Lu |
| 2018 | COMPSAC | Formalization and Verification of Mobile Systems Calculus Using the Rewriting Engine Maude. | Wanling Xie, Huibiao Zhu, Min Zhang, Gang Lu, Yucheng Fang |
| 2018 | FedCSIS | Assertional Reasoning for Concurrent and Communicating BPEL-like Programs. | Longfei Zhu, Qiwen Xu, Huibiao Zhu |
| 2018 | ICFEM | Modeling and Verifying NDN Access Control Using CSP. | Yuan Fei, Huibiao Zhu |
| 2018 | ICFEM | UTP Semantics for BigrTiMo. | Wanling Xie, Huibiao Zhu, Shengchao Qin |
| 2018 | SAC | Modeling and verifying SDN with multiple controllers. | Lili Xiao, Shuangqing Xiang, Huibiao Zhu |
| 2018 | SEKE | Modeling and Verifying Leader Election Algorithm in CSP (S). | Yucheng Fang, Huibiao Zhu, Huiwen Wang |
| 2018 | SEKE | Security Analysis of the Access Control Solution of NDN Using BAN Logic (S). | Yuan Fei, Huibiao Zhu, Huiwen Wang |
| 2018 | SEKE | Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP. | Huiwen Wang, Huibiao Zhu, Yuan Fei, Lili Xiao |
| 2018 | TASE | A Fully Abstract Encoding for Sub Asynchronous Pi Calculus. | Wenjun Du, Zhengfeng Yang, Huibiao Zhu |
| 2018 | TASE | Modeling and Verification of NLSR Protocol using UPPAAL. | Yuan Fei, Huibiao Zhu, Xin Li |
| 2018 | TASE | Modeling and Verifying TopoGuard in OpenFlow-Based Software Defined Networks. | Shuangqing Xiang, Huibiao Zhu, Lili Xiao, Wanling Xie |
| 2017 | APSEC | Formalization and Verification of the PSTM Architecture. | Ailun Liu, Miroslav Popovic, Huibiao Zhu |
| 2017 | APSEC | Modeling and Verifying Identity Authentication Security of HDFS Using CSP. | Chao Xu, Huibiao Zhu, Wanling Xie |
| 2017 | COMPSAC | Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. | Ailun Liu, Huibiao Zhu, Yuan Fei, Shuangqing Xiang, Gang Lu, Wanling Xie |
| 2017 | COMPSAC | A Proof System for mCWQ. | Wanling Xie, Xi Wu, Huibiao Zhu, Gang Lu, Ailun Liu |
| 2017 | COMPSAC | Formalization and Verification of the PKMv3 Protocol Using CSP. | Yuanmin Xu, Huibiao Zhu, Xiaoran Zhu, Xi Wu, Jian Guo, Gang Lu |
| 2017 | FedCSIS | A Proof System for MDESL. | Jianyu Lu, Wanling Xie, Huibiao Zhu, Yuan Fei |
| 2017 | ICECCS | BigrTiMo-A Process Algebra for Structure-Aware Mobile Systems. | Wanling Xie, Huibiao Zhu, Qiwen Xu |
| 2016 | APSEC | Model-Based Continuous Verification. | Lingling Fan, Sen Chen, Lihua Xu, Zongyuan Yang, Huibiao Zhu |
| 2016 | COMPSAC | Modeling and Verifying HDFS Using CSP. | Wanling Xie, Huibiao Zhu, Xi Wu, Shuangqing Xiang, Jian Guo |
| 2016 | ICFEM | An SMT-Based Approach to the Formal Analysis of MARTE/CCSL. | Min Zhang, Frdric Mallet, Huibiao Zhu |
| 2015 | ICECCS | A Formal Framework for Reasoning Emergent Behaviors in Swarm Robotic Systems. | Qin Li, Jinxun Wang, Qiwen Xu, Yanhong Huang, Huibiao Zhu |
| 2015 | TASE | A SAT-Based Analysis of a Calculus for Wireless Sensor Networks. | Xi Wu, Hanne Riis Nielson, Huibiao Zhu |
| 2015 | TASE | Formal Verification of PKMv3 Protocol Using DT-Spin. | Xiaoran Zhu, Yuanmin Xu, Jian Guo, Xi Wu, Huibiao Zhu, Weikai Miao |
| 2014 | APSEC | pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems. | Xin Li, Yanhong Huang, Jianqi Shi, Jian Guo, Huibiao Zhu, Yuanmin Xu |
| 2014 | PRDC | Reasoning about Group-Based Mobility in MANETs. | Xi Wu, Si Liu, Huibiao Zhu, Yongxin Zhao |
| 2014 | TASE | Configuration of Services Based on Virtualization. | Jianmin Jiang, Huibiao Zhu, Qin Li, Shi Zhang, Ping Gong, Zhong Hong |
| 2014 | TASE | Modeling and Verifying the TTCAN Protocol Using Timed CSP. | Qinwen Ran, Xi Wu, Xin Li, Jianqi Shi, Jian Guo, Huibiao Zhu |
| 2013 | APSEC | Linking the Semantics of BPEL Using Maude. | Peng Liu, Huibiao Zhu, Shengchao Qin, Phillip J. Brooke, Xi Wu |
| 2013 | ICECCS | Linking Algebraic Semantics and Operational Semantics for Web Services Using Maude. | Peng Liu, Huibiao Zhu, Shengchao Qin, Phillip J. Brooke, Xi Wu |
| 2013 | ICECCS | Formal Modelling and Analysis of AODV. | Xiaofeng Wu, Jeff W. Sanders, Huibiao Zhu |
| 2013 | ICFEM | Linking Operational Semantics and Algebraic Semantics for Wireless Networks. | Xiaofeng Wu, Huibiao Zhu |
| 2013 | ICST | A Denotational Model for Interrupt-Driven Programs. | Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu |
| 2013 | TASE | Formal Analysis of AODV Using Rely-Guarantee. | Xiaofeng Wu, Qiwen Xu, Huibiao Zhu |
| 2013 | TASE | A Timing Verification Framework for AUTOSAR OS Component Development Based on Real-Time Maude. | Longfei Zhu, Peng Liu, Jianqi Shi, Zheng Wang, Huibiao Zhu |
| 2012 | ICECCS | ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System. | Jianqi Shi, Jifeng He, Huibiao Zhu, Huixing Fang, Yanhong Huang, Xiaoxian Zhang |
| 2012 | ICECCS | xBIL - A Hardware Resource Oriented Binary Intermediate Language. | Jianqi Shi, Longfei Zhu, Huixing Fang, Jian Guo, Huibiao Zhu, Xin Ye |
| 2012 | ICFEM | Complementary Methodologies for Developing Hybrid Systems with Event-B. | Wen Su, Jean-Raymond Abrial, Huibiao Zhu |
| 2012 | SEFM | A Denotational Model for Instantaneous Signal Calculus. | Yongxin Zhao, Longfei Zhu, Huibiao Zhu, Jifeng He |
| 2012 | SEFM | The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs. | Huibiao Zhu, Qiwen Xu, Chris Ma, Shengchao Qin, Zongyan Qiu |
| 2012 | TASE | Formal Verification and Simulation: Co-verification for Subway Control Systems. | Huixing Fang, Jian Guo, Huibiao Zhu, Jianqi Shi |
| 2012 | TASE | Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System. | Jianqi Shi, Longfei Zhu, Yanhong Huang, Jian Guo, Huibiao Zhu, Huixing Fang, Xin Ye |
| 2012 | TASE | Modelling and Analysis of Smart Grid: A Stochastic Model Checking Case Study. | Ender Yksel, Huibiao Zhu, Hanne Riis Nielson, Heqing Huang, Flemming Nielson |
| 2011 | COMPSAC | Formal Approaches to Mode Conversion and Positioning for Vehicle System. | Wen Su, Fan Yang, Xiaofeng Wu, Jian Guo, Huibiao Zhu |
| 2011 | ICFEM | From Requirements to Development: Methodology and Example. | Wen Su, Jean-Raymond Abrial, Runlei Huang, Huibiao Zhu |
| 2011 | TASE | Modeling and Verifying the Code-Level OSEK/VDX Operating System with CSP. | Yanhong Huang, Yongxin Zhao, Longfei Zhu, Qin Li, Huibiao Zhu, Jianqi Shi |
| 2011 | TASE | Towards a Probabilistic Calculus for Mobile Ad Hoc Networks. | Si Liu, Yongxin Zhao, Huibiao Zhu, Qin Li |
| 2011 | TASE | Towards an Axiomatic Verification System for JavaScript. | Shengchao Qin, Aziem Chawdhary, Wei Xiong, Malcolm Munro, Zongyan Qiu, Huibiao Zhu |
| 2011 | TASE | Modeling and Analyzing the (mu)TESLA Protocol Using CSP. | Mengying Wang, Huibiao Zhu, Yongxin Zhao, Si Liu |
| 2011 | TASE | Formalizing Application Programming Interfaces of the OSEK/VDX Operating System Specification. | Longfei Zhu, Min Zhang, Yanhong Huang, Jianqi Shi, Huibiao Zhu |
| 2010 | ICDCIT | Formal Approaches to Location Management in Mobile Communications. | Juanhua Kang, Qin Li, Huibiao Zhu, Wenjuan Wu |
| 2010 | ICTAC | A Denotational Semantical Model for Orc Language. | Qin Li, Huibiao Zhu, Jifeng He |
| 2010 | TASE | Probabilistic Model of System Survivability. | Yongxin Zhao, Yanhong Huang, Jianwen Li, Huibiao Zhu |
| 2010 | TASE | A Formal Model for Service Choreography with Exception Handling and Finalization. | Yongxin Zhao, Zheng Wang, Geguang Pu, Huibiao Zhu |
| 2009 | SEW | Towards Specification and Refinement of Contracts with Environment Changes. | Qin Li, Huibiao Zhu |
| 2009 | SEW | Animating the Link Between Operational Semantics and Algebraic Semantics for a Probabilistic Timed Shared-Variable Language. | Huibiao Zhu, Fan Yang, Jifeng He, Jonathan P. Bowen, Jeff W. Sanders |
| 2009 | TASE | Formal Approaches to Deadlock Analysis in Competitions of Shared Web Resources. | Jieqi Ding, Han Zhu, Huibiao Zhu, Qin Li |
| 2009 | TASE | Modeling MapReduce with CSP. | Wen Su, Fan Yang, Huibiao Zhu, Qin Li |
| 2008 | APSEC | Execution Semantics for rCOS. | Zheng Wang, Xiao Yu, Geguang Pu, Libo Feng, Huibiao Zhu, Jifeng He |
| 2008 | FORTE | Specifying and Verifying Web Transactions. | Jing Li, Huibiao Zhu, Jifeng He |
| 2008 | ICDCIT | A Denotational Model for Web Services Choreography. | Geguang Pu, Yongxin Zhao, Zheng Wang, Libo Feng, Huibiao Zhu, Jifeng He |
| 2008 | ICTAC | An Observational Model for Transactional Calculus of Services Orchestration. | Jing Li, Huibiao Zhu, Jifeng He |
| 2008 | ISoLA | ASERE: Assuring the Satisfiability of Sequential Extended Regular Expressions. | Naiyong Jin, Huibiao Zhu |
| 2007 | ICDCIT | Unifying Denotational Semantics with Operational Semantics for Web Services. | Huibiao Zhu, Jifeng He, Jing Li |
| 2007 | ICECCS | A Formal Model for Compensable Transactions. | Jing Li, Huibiao Zhu, Geguang Pu, Jifeng He |
| 2007 | ICTAC | Algebraic Semantics for Compensable Transactions. | Jing Li, Huibiao Zhu, Jifeng He |
| 2007 | SEFM | Algebraic Approach to Linking the Semantics of Web Services. | Huibiao Zhu, Jifeng He, Jing Li, Jonathan P. Bowen |
| 2007 | SEW | Modeling and Verifying Web Services Choreography Using Process Algebra. | Jing Li, Jifeng He, Huibiao Zhu, Geguang Pu |
| 2007 | SEW | An Inconsistency Free Formalization of B/S Architecture. | Qin Li, Huibiao Zhu, Jifeng He |
| 2007 | SEW | Looking into Compensable Transactions. | Jing Li, Huibiao Zhu, Geguang Pu, Jifeng He |
| 2007 | SEW | Algebraic Approach to Operational Semantics and Observation-Oriented Semantics for a Timed Shared-Variable Language with Probability. | Huibiao Zhu, Jifeng He, Jonathan P. Bowen |
| 2007 | SEW | An Operational Approach to BPEL-like Programming. | Huibiao Zhu, Jifeng He, Geguang Pu, Jing Li |
| 2007 | TASE | Conformance Validation between Choreography and Orchestration. | Jing Li, Huibiao Zhu, Geguang Pu |
| 2006 | ICECCS | From Algebraic Semantics to Denotational Semantics for Verilog. | Huibiao Zhu, Jifeng He, Jonathan P. Bowen |
| 2006 | ICFEM | Towards the Semantics for Web Service Choreography Description Language. | Jing Li, Jifeng He, Geguang Pu, Huibiao Zhu |
| 2006 | ISoLA | Patterns with Algebraic Properties in BPEL0. | Geguang Pu, Huibiao Zhu, Jifeng He, Zongyan Qiu, Hongli Yang, Xiangpeng Zhao |
| 2006 | SEW | An Operational Semantics of an Event-Driven System-Level Simulator. | Xiaoqing Peng, Huibiao Zhu, Jifeng He, Naiyong Jin |
| 2006 | SEW | Integrating Probability with Time and Shared-Variable Concurrency. | Huibiao Zhu, Shengchao Qin, Jifeng He, Jonathan P. Bowen |
| 2002 | ICFEM | Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics. | Huibiao Zhu, Jonathan P. Bowen, Jifeng He |
| 2001 | APSEC | Deriving Operational Semantics from Denotational Semantics for Verilog. | Huibiao Zhu, Jonathan P. Bowen, Jifeng He |