Super-polynomial quantum speed-ups for boolean evaluation trees with hidden structure. - Bohua Zhan; Shelby Kimmel; Avinatan Hassidim (ITCS, 2012)

AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. - Bohua Zhan (ITP, 2016)

Automation of separation logic using auto2. - Bohua Zhan (CoRR, 2016)

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. - Bohua Zhan; Maximilian P. L. Haslbeck (IJCAR, 2018)

Efficient Verification of Imperative Programs Using Auto2. - Bohua Zhan (TACAS (1), 2018)

Smooth Manifolds. - Fabian Immler; Bohua Zhan (Arch. Formal Proofs, 2018)

Auto2 Prover. - Bohua Zhan (Arch. Formal Proofs, 2018)

Verifying Imperative Programs using Auto2. - Bohua Zhan (Arch. Formal Proofs, 2018)

NIL: Learning Nonlinear Interpolants. - Mingshuai Chen; Jian Wang 042; Jie An 001; Bohua Zhan; Deepak Kapur; Naijun Zhan (CADE, 2019)

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (CAV (2), 2019)

Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. - Fabian Immler; Bohua Zhan (CPP, 2019)

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Andrew Sogokon; Yong Kiam Tan; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH@CPSIoTWeek, 2019)

Design of Point-and-Click User Interfaces for Proof Assistants. - Bohua Zhan; Zhenyan Ji; Wenfan Zhou; Chaozhu Xiang; Jie Hou; Wenhui Sun (ICFEM, 2019)

Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (Arch. Formal Proofs, 2019)

holpy: Interactive Theorem Proving in Python. - Bohua Zhan (CoRR, 2019)

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. - Bohua Zhan (J. Autom. Reason., 2019)

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Jonathan Julián Huerta y Munive; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH, 2020)

PAC Learning of Deterministic One-Clock Timed Automata. - Wei Shen; Jie An 001; Bohua Zhan; Miaomiao Zhang 003; Bai Xue 001; Naijun Zhan (ICFEM, 2020)

Learning One-Clock Timed Automata. - Jie An 001; Mingshuai Chen; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (TACAS (1), 2020)

Modelling and Verification of Real-Time Publish and Subscribe Protocol Using Uppaal and Simulink/Stateflow. - Qianqian Lin; Shuling Wang; Bohua Zhan; Bin Gu (J. Comput. Sci. Technol., 2020)

ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH@ADHS, 2021)

Verified Interactive Computation of Definite Integrals. - Runqing Xu; Liming Li; Bohua Zhan (CADE, 2021)

Formal Verification of Consensus in the Taurus Distributed Database. - Song Gao 014; Bohua Zhan; Depeng Liu; Xuechao Sun; Yanan Zhi; David N. Jansen; Lijun Zhang 001 (FM, 2021)

Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. - Bohua Zhan; Bin Gu 006; Xiong Xu; Xiangyu Jin; Shuling Wang 003; Bai Xue 001; Xiaofeng Li; Yao Chen; Mengfei Yang; Naijun Zhan (RTAS, 2021)

Formal Analysis of 5G AKMA. - Tengshun Yang; Shuling Wang 003; Bohua Zhan; Naijun Zhan; Jinghui Li; Shuangqing Xiang; Zhan Xiang; Bifei Mao (SETTA, 2021)

Learning real-time automata. - Jie An 001; Lingtai Wang; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Sci. China Inf. Sci., 2021)

Inferring Switched Nonlinear Dynamical Systems. - Xiangyu Jin; Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Formal Aspects Comput., 2021)

Learning Nondeterministic Real-Time Automata. - Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (ACM Trans. Embed. Comput. Syst., 2021)

ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Bohua Zhan; Huanhuan Sheng; Alexander Bentkamp; Xiangyu Jin; Shuling Wang 003; Simon Foster 001; Christian Pardillo Laursen; Jonathan Julián Huerta y Munive (ARCH@SAFECOMP, 2022)

Learning Deterministic One-Clock Timed Automata via Mutation Testing. - Xiaochen Tang; Wei Shen; Miaomiao Zhang 003; Jie An 001; Bohua Zhan; Naijun Zhan (ATVA, 2022)

Active Learning of One-Clock Timed Automata Using Constraint Solving. - Runqing Xu; Jie An 001; Bohua Zhan (ATVA, 2022)

Machine-Checked Executable Semantics of Stateflow. - Shicheng Yi; Shuling Wang 003; Bohua Zhan; Naijun Zhan (ICFEM, 2022)

User Interface Design in the HolPy Theorem Prover (Invited Talk). - Bohua Zhan (ITP, 2022)

Compositional Verification of Interacting Systems Using Event Monads. - Bohua Zhan; Yi Lv; Shuling Wang; Gehang Zhao; Jifeng Hao; Hong Ye; Bican Xia (ITP, 2022)

Translating a large subset of stateflow to hybrid CSP with code optimization. - Panhua Guo; Bohua Zhan; Xiong Xu; Shuling Wang; Wenhui Sun (J. Syst. Archit., 2022)

Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). - Tengshun Yang; Shuling Wang 003; Bohua Zhan; Naijun Zhan; Jinghui Li; Shuangqing Xiang; Zhan Xiang; Bifei Mao (J. Syst. Archit., 2022)

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. - Xiong Xu; Shuling Wang 003; Bohua Zhan; Xiangyu Jin; Jean-Pierre Talpin; Naijun Zhan (Theor. Comput. Sci., 2022)

ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Huanhuan Sheng; Bohua Zhan; Shuling Wang 003; Simon Foster 001; Jonathan Julián Huerta y Munive (ARCH, 2023)

Iscalc: An Interactive Symbolic Computation Framework (System Description). - Bohua Zhan; Yuheng Fan; Weiqiang Xiong; Runqing Xu (CADE, 2023)

HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. - Huanhuan Sheng; Alexander Bentkamp; Bohua Zhan (FM, 2023)

VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. - Qiaowen Jia; Yi Lv; Peng Wu 002; Bohua Zhan; Jifeng Hao; Hong Ye; Chao Wang 069 (TASE, 2023)

A Generalized Hybrid Hoare Logic. - Naijun Zhan; Bohua Zhan; Shuling Wang 003; Dimitar P. Guelev; Xiangyu Jin (CoRR, 2023)

Compression of enumerations and gain. - George Barmpalias; Xiaoyan Zhang; Bohua Zhan (CoRR, 2023)

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

A denotational semantics of Simulink with higher-order UTP. - Xiong Xu; Bohua Zhan; Shuling Wang 003; Jean-Pierre Talpin; Naijun Zhan (J. Log. Algebraic Methods Program., 2023)

Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Bohua Zhan; Naijun Zhan (ACM Trans. Softw. Eng. Methodol., 2023)

Verifying Randomized Consensus Protocols with Common Coins. - Song Gao 014; Bohua Zhan; Zhilin Wu; Lijun Zhang 001 (DSN, 2024)

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. - Shuling Wang 003; Zekun Ji; Xiong Xu; Bohua Zhan; Qiang Gao; Naijun Zhan (ICCPS, 2024)

Efficient Local Search for Nonlinear Real Arithmetic. - Zhonghan Wang; Bohua Zhan; Bohan Li 002; Shaowei Cai 001 (VMCAI (1), 2024)

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. - Bohua Zhan; Xiong Xu; Qiang Gao; Zekun Ji; Xiangyu Jin; Shuling Wang 003; Naijun Zhan (CoRR, 2024)

OSVAuto: semi-automatic verifier for functional specifications of operating systems. - Yulun Wu; Bohua Zhan; Bican Xia (CoRR, 2024)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. - Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (CoRR, 2024)

Mechanizing the CMP Abstraction for Parameterized Verification. - Yongjian Li; Bohua Zhan; Jun Pang 001 (Proc. ACM Program. Lang., 2024)

Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System. - Xiong Xu; Shuling Wang 003; Zekun Ji; Qiang Gao; Xiangyu Jin; Bohua Zhan; Naijun Zhan (The Practice of Formal Methods (II), 2024)

HpC: A Calculus for Hybrid and Mobile Systems. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Hao Wu 085; Bohua Zhan; Xinxin Liu; Naijun Zhan (Proc. ACM Program. Lang., 2025)

HpC: A Calculus for Hybrid and Mobile Systems - Full Version. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Hao Wu 085; Bohua Zhan; Xinxin Liu; Naijun Zhan (CoRR, 2025)

KBX: Verified Model Synchronization via Formal Bidirectional Transformation. - Jianhong Zhao; Yongwang Zhao; Peisen Yao; Fanlang Zeng; Bohua Zhan; Kui Ren 001 (ACM Trans. Softw. Eng. Methodol., 2025)