Bohua Zhan

Associate Research Professor
State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences

Office: Room 219, Building 5
Address: No. 4, South Fourth Street, Zhong Guan Cun, Beijing, 100190, China
Email: [email protected]

Current interests

• Interactive theorem proving, including application to program verification and formalization of mathematics.
• Modelling and verification of hybrid systems.
• Verification of quantum algorithms.

Code

• holpy: Interactive theorem proving in Python. gitee github
• Auto2: Saturation-based prover implemented in Isabelle. github
• QHLProver: Verification of quantum algorithms using Quantum Hoare Logic. AFP

Publications (dblp)

Journal Articles

• Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan (2023):
  Semantics Foundation for Cyber-physical Systems Using Higher-order UTP
  ACM Transactions on Software Engineering and Methodology 32(1): 9:1-9:48 published version
• Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan (2023):
  A denotational semantics of Simulink with higher-order UTP
  J. Logical and Algebraic Methods in Programming 130: 100809 published version
• Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao (2022):
  Formal Analysis of 5G Authentication and Key Management for Applications (AKMA)
  J. System Architecture 126: 102478 (extended version of paper in SETTA 2021) published version
• Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan (2022):
  Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow
  Theoretical Computer Science 903: 1-25 published version
• Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2021):
  Learning Nondeterministic Real-Time Automata
  ACM Transactions on Embedded Computing Systems 20(5s): 99:1-99-26 published version (open access)
• Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2021):
  Inferring Switched Nonlinear Dynamical Systems
  Formal Aspects of Computing 33(3): 385-406 published version
• Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2021):
  Learning real-time automata
  Science China Information Sciences 64(9) published version
• Qianqian Lin, Shuling Wang, Bohua Zhan, Bin Gu (2020):
  Modelling and Verification of the RTPS Protocol using Uppaal and Simulink/Stateflow.
  J. Computer Science and Technology 35(6): 1324-1342 published version appendix
• Bohua Zhan (2019):
  Formalization of the fundamental group in untyped set theory using auto2.
  J. Automated Reasoning 63(2): 517-538 (extended version of paper in ITP 2017) published version

Conference Papers / Talks

• Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
  HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
  Formal Methods (FM 2023) published version arXiv
• Runqing Xu, Jie An, Bohua Zhan
  Active Learning of One-Clock Timed Automata using Constraint Solving
  Automated Technology for Verification and Analysis (ATVA 2022) published version arXiv
• Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan
  Learning Deterministic One-Clock Timed Automata via Mutation Testing
  Automated Technology for Verification and Analysis (ATVA 2022) published version
• Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
  Machine-checked executable semantics of Stateflow
  International Conference on Formal Engineering Methods (ICFEM 2022) published version arXiv
• Bohua Zhan
  User Interface Design in the HolPy Theorem Prover (Invited Talk)
  Interactive Theorem Proving (ITP 2022) published version (open access) slides
• Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia
  Compositional Verification of Interacting Systems Using Event Monads
  Interactive Theorem Proving (ITP 2022) published version (open access) slides
• Panhua Guo, Bohua Zhan, Xiong Xu, Shuling Wang, Wenhui Sun
  Translating a Large Subset of Stateflow to Hybrid CSP with Code Optimization
  Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2021) published version
• Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
  Formal Analysis of 5G AKMA
  Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2021) published version
• Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang (2021):
  Formal Verification of Consensus in the Taurus Distributed Database
  Formal Methods (FM 2021 I-Day) published version
• Runqing Xu, Liming Li, Bohua Zhan (2021):
  Verified Interactive Computation of Definite Integrals
  Conference on Automated Deduction (CADE 2021) paper slides
• Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan (2021):
  Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander
  Real-Time and Embedded Technology and Applications Symposium (RTAS 2021) published version
• Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, and Naijun Zhan (2020):
  PAC Learning of Deterministic One-Clock Timed Automata
  International Conference on Formal Engineering Methods (ICFEM 2020) paper
• Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang (2020):
  Learning One-Clock Timed Automata.
  Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020) arXiv slides
• Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun (2019):
  Design of Point-and-Click User Interfaces for Proof Assistants.
  International Conference on Formal Engineering Methods (ICFEM 2019) paper slides
• Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan (2019):
  NIL: Learning Nonlinear Interpolants.
  Conference on Automated Deduction (CADE 2019) arXiv slides
• Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan (2019):
  Formal Verification of Quantum Algorithms Using Quantum Hoare Logic.
  Computer Aided Verification (CAV 2019) paper slides AFP
• Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan (2019):
  ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving.
  Applied Verification of Continuous and Hybrid Systems (ARCH@CPSIoTWeek 2019) paper
• Fabian Immler, Bohua Zhan (2019):
  Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.
  Certified Programs and Proofs (CPP 2019) paper AFP
• Bohua Zhan, Maximilian P. L. Haslbeck (2018):
  Verifying asymptotic time complexity of imperative programs in Isabelle.
  International Joint Conference on Automated Reasoning (IJCAR 2018) arXiv slides repository
• Bohua Zhan (2018):
  Efficient verification of imperative programs using auto2.
  Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018) arXiv slides
• Bohua Zhan (2017):
  Formalization of the fundamental group in untyped set theory using auto2.
  Interactive Theorem Proving (ITP 2017) arXiv slides
• Bohua Zhan (2016):
  AUTO2, a saturation-based heuristic prover for higher-order logic.
  Interactive Theorem Proving (ITP 2016) arXiv slides
• Bohua Zhan, Shelby Kimmel, Avinatan Hassidim (2012):
  Super-polynomial quantum speed-ups for boolean evaluation trees with hidden structure.
  Innovations in Theoretical Computer Science (ITCS 2012) arXiv

Talks

• Proof automation in set theory. (June 2018)
  Conference in honour of Thomas C. Hales on the occasion of his 60th birthday. slides

Past work

Code

• bfh_python: Computations in bordered Floer homology.

Journal Articles

• Bohua Zhan (2016)
  Combinatorial proofs in bordered Heegaard Floer homology.
  Algebr. Geom. Topol. 16 (2016) 2571-2636 arXiv published version
• Bohua Zhan (2016)
  Explicit Koszul-dualizing bimodules in bordered Heegaard Floer homology.
  Algebr. Geom. Topol. 16 (2016) 231-266 arXiv published version