| 2025 | ICECCS | Checking Linearizability of Multi-core Task Management and Scheduling System. | Qiaowen Jia, Liangjie Lv, Yuting Yang, Bohua Zhan, Peng Wu, Jifeng Hao, Hong Ye, Chao Wang, Yi Lv |
| 2025 | SETTA | HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. | Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan |
| 2024 | DSN | Verifying Randomized Consensus Protocols with Common Coins. | Song Gao, Bohua Zhan, Zhilin Wu, Lijun Zhang |
| 2024 | VMCAI | Efficient Local Search for Nonlinear Real Arithmetic. | Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai |
| 2023 | CADE | Iscalc: An Interactive Symbolic Computation Framework (System Description). | Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu |
| 2023 | FM | HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. | Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan |
| 2023 | TASE | VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. | Qiaowen Jia, Yi Lv, Peng Wu, Bohua Zhan, Jifeng Hao, Hong Ye, Chao Wang |
| 2022 | ATVA | Learning Deterministic One-Clock Timed Automata via Mutation Testing. | Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan |
| 2022 | ATVA | Active Learning of One-Clock Timed Automata Using Constraint Solving. | Runqing Xu, Jie An, Bohua Zhan |
| 2022 | ICFEM | Machine-Checked Executable Semantics of Stateflow. | Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan |
| 2022 | ITP | User Interface Design in the HolPy Theorem Prover (Invited Talk). | Bohua Zhan |
| 2022 | ITP | Compositional Verification of Interacting Systems Using Event Monads. | Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia |
| 2021 | CADE | Verified Interactive Computation of Definite Integrals. | Runqing Xu, Liming Li, Bohua Zhan |
| 2021 | FM | Formal Verification of Consensus in the Taurus Distributed Database. | Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang |
| 2021 | RTAS | Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. | Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan |
| 2021 | SETTA | Translating a Large Subset of Stateflow to Hybrid CSP with Code Optimization. | Panhua Guo, Bohua Zhan, Xiong Xu, Shuling Wang, Wenhui Sun |
| 2021 | SETTA | Formal Analysis of 5G AKMA. | Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao |
| 2020 | ICFEM | PAC Learning of Deterministic One-Clock Timed Automata. | Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan |
| 2020 | TACAS | Learning One-Clock Timed Automata. | Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang |
| 2019 | CADE | NIL: Learning Nonlinear Interpolants. | Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan |
| 2019 | CAV | Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. | Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan |
| 2019 | CPP | Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. | Fabian Immler, Bohua Zhan |
| 2019 | ICFEM | Design of Point-and-Click User Interfaces for Proof Assistants. | Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun |
| 2018 | CADE | Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. | Bohua Zhan, Maximilian P. L. Haslbeck |
| 2018 | TACAS | Efficient Verification of Imperative Programs Using Auto2. | Bohua Zhan |
| 2017 | ITP | Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. | Bohua Zhan |
| 2016 | ITP | AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. | Bohua Zhan |