Bohua Zhan

According to our database, Bohua Zhan authored at least 48 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

OSVAuto: semi-automatic verifier for functional specifications of operating systems.

Yulun Wu, Bohua Zhan, Bican Xia

CoRR, 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, Naijun Zhan

CoRR, 2024

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes.

Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan

CoRR, 2024

Efficient Local Search for Nonlinear Real Arithmetic.

Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

2023

Semantics Foundation for Cyber-physical Systems Using Higher-order UTP.

Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan

ACM Trans. Softw. Eng. Methodol., January, 2023

A denotational semantics of Simulink with higher-order UTP.

Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan

J. Log. Algebraic Methods Program., 2023

Preface to the Special Issue on Constraint Solving and Theorem Proving.

Shaowei Cai, Zhenbang Chen, Ji Wang, Bohua Zhan, Yongwang Zhao

Int. J. Softw. Informatics, 2023

Compression of enumerations and gain.

George Barmpalias, Xiaoyan Zhang, Bohua Zhan

CoRR, 2023

A Generalized Hybrid Hoare Logic.

Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin

CoRR, 2023

VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects.

Qiaowen Jia, Yi Lv, Peng Wu, Bohua Zhan, Jifeng Hao, Hong Ye, Chao Wang

Proceedings of the Theoretical Aspects of Software Engineering, 2023

HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic.

Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan

Proceedings of the Formal Methods - 25th International Symposium, 2023

Iscalc: An Interactive Symbolic Computation Framework (System Description).

Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow.

Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan

Theor. Comput. Sci., 2022

Formal Analysis of 5G Authentication and Key Management for Applications (AKMA).

Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao

J. Syst. Archit., 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

Compositional Verification of Interacting Systems Using Event Monads.

Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

User Interface Design in the HolPy Theorem Prover (Invited Talk).

Bohua Zhan

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Machine-Checked Executable Semantics of Stateflow.

Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan

Proceedings of the Formal Methods and Software Engineering, 2022

Active Learning of One-Clock Timed Automata Using Constraint Solving.

Runqing Xu, Jie An, Bohua Zhan

Proceedings of the Automated Technology for Verification and Analysis, 2022

Learning Deterministic One-Clock Timed Automata via Mutation Testing.

Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan

Proceedings of the Automated Technology for Verification and Analysis, 2022

2021

Learning Nondeterministic Real-Time Automata.

Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

ACM Trans. Embed. Comput. Syst., 2021

Inferring Switched Nonlinear Dynamical Systems.

Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Formal Aspects Comput., 2021

Learning real-time automata.

Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Sci. China Inf. Sci., 2021

Formal Analysis of 5G AKMA.

Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2021

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

Proceedings of the 27th IEEE Real-Time and Embedded Technology and Applications Symposium, 2021

Formal Verification of Consensus in the Taurus Distributed Database.

Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang

Proceedings of the Formal Methods - 24th International Symposium, 2021

Verified Interactive Computation of Definite Integrals.

Runqing Xu, Liming Li, Bohua Zhan

Proceedings of the Automated Deduction - CADE 28, 2021

ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), 2021

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

Learning One-Clock Timed Automata.

Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

PAC Learning of Deterministic One-Clock Timed Automata.

Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan

Proceedings of the Formal Methods and Software Engineering, 2020

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

2019

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2.

Bohua Zhan

J. Autom. Reason., 2019

holpy: Interactive Theorem Proving in Python.

Bohua Zhan

CoRR, 2019

Quantum Hoare Logic.

Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan

Arch. Formal Proofs, 2019

Design of Point-and-Click User Interfaces for Proof Assistants.

Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun

Proceedings of the Formal Methods and Software Engineering, 2019

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.

Fabian Immler, Bohua Zhan

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

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

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

NIL: Learning Nonlinear Interpolants.

Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Verifying Imperative Programs using Auto2.

Bohua Zhan

Arch. Formal Proofs, 2018

Auto2 Prover.

Bohua Zhan

Arch. Formal Proofs, 2018

Smooth Manifolds.

Fabian Immler, Bohua Zhan

Arch. Formal Proofs, 2018

Efficient Verification of Imperative Programs Using Auto2.

Bohua Zhan

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.

Bohua Zhan, Maximilian P. L. Haslbeck

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2016

Automation of separation logic using auto2.

Bohua Zhan

CoRR, 2016

AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic.

Bohua Zhan

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2012

Super-polynomial quantum speed-ups for boolean evaluation trees with hidden structure.

Bohua Zhan, Shelby Kimmel, Avinatan Hassidim

Proceedings of the Innovations in Theoretical Computer Science 2012, 2012