Bohua Zhan

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 64

Top Topics

Formal Verification

Theorem Proving

Imperative Programs

Top Venues

Arch. Formal Proofs

Publications

Yulun Wu, Bohua Zhan, Bican Xia
OSVAuto: semi-automatic verifier for functional specifications of operating systems. CoRR (2024)
Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. CoRR (2024)
Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao, Naijun Zhan
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. ICCPS (2024)
Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. CoRR (2024)
Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai
Efficient Local Search for Nonlinear Real Arithmetic. VMCAI (1) (2024)
Yongjian Li, Bohua Zhan, Jun Pang
Mechanizing the CMP Abstraction for Parameterized Verification. Proc. ACM Program. Lang. 8 (OOPSLA1) (2024)
Bohua Zhan, Xiong Xu, Qiang Gao, Zekun Ji, Xiangyu Jin, Shuling Wang, Naijun Zhan
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. CoRR (2024)
Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, Kui Ren
KBX: Verified Model Synchronization via Formal Bidirectional Transformation. CoRR (2024)
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. FM (2023)
Stefan Mitsch, Huanhuan Sheng, Bohua Zhan, Shuling Wang, Simon Foster, Jonathan Julián Huerta y Munive
ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving. ARCH (2023)
Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan
A denotational semantics of Simulink with higher-order UTP. J. Log. Algebraic Methods Program. 130 (2023)
Qiaowen Jia, Yi Lv, Peng Wu, Bohua Zhan, Jifeng Hao, Hong Ye, Chao Wang
VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. TASE (2023)
Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu
Iscalc: An Interactive Symbolic Computation Framework (System Description). CADE (2023)
Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai
Efficient Local Search for Nonlinear Real Arithmetic. CoRR (2023)
Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan
Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. ACM Trans. Softw. Eng. Methodol. 32 (1) (2023)
Shaowei Cai, Zhenbang Chen, Ji Wang, Bohua Zhan, Yongwang Zhao
Preface to the Special Issue on Constraint Solving and Theorem Proving. Int. J. Softw. Informatics 13 (3) (2023)
George Barmpalias, Xiaoyan Zhang, Bohua Zhan
Compression of enumerations and gain. CoRR (2023)
Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin
A Generalized Hybrid Hoare Logic. CoRR (2023)
Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
Machine-Checked Executable Semantics of Stateflow. ICFEM (2022)
Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen, Jonathan Julián Huerta y Munive
ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. ARCH@SAFECOMP (2022)
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic. CoRR (2022)
Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
Machine-checked executable semantics of Stateflow. CoRR (2022)
Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan
Learning Deterministic One-Clock Timed Automata via Mutation Testing. ATVA (2022)
Runqing Xu, Jie An, Bohua Zhan
Active Learning of One-Clock Timed Automata using Constraint Solving. CoRR (2022)
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). J. Syst. Archit. 126 (2022)
Panhua Guo, Bohua Zhan, Xiong Xu, Shuling Wang, Wenhui Sun
Translating a large subset of stateflow to hybrid CSP with code optimization. J. Syst. Archit. 130 (2022)
Bohua Zhan
User Interface Design in the HolPy Theorem Prover (Invited Talk). ITP (2022)
Runqing Xu, Jie An, Bohua Zhan
Active Learning of One-Clock Timed Automata Using Constraint Solving. ATVA (2022)
Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan
Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theor. Comput. Sci. 903 (2022)
Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia
Compositional Verification of Interacting Systems Using Event Monads. ITP (2022)
Runqing Xu, Liming Li, Bohua Zhan
Verified Interactive Computation of Definite Integrals. CADE (2021)
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
Formal Analysis of 5G AKMA. SETTA (2021)
Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang
Formal Verification of Consensus in the Taurus Distributed Database. FM (2021)
Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan
Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. RTAS (2021)
Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS (2021)
Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. 33 (3) (2021)
Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning real-time automata. Sci. China Inf. Sci. 64 (9) (2021)
Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. 20 (5s) (2021)
Panhua Guo, Bohua Zhan, Xiong Xu, Shuling Wang, Wenhui Sun
Translating a Large Subset of Stateflow to Hybrid CSP with Code Optimization. SETTA (2021)
Qianqian Lin, Shuling Wang, Bohua Zhan, Bin Gu
Modelling and Verification of Real-Time Publish and Subscribe Protocol Using Uppaal and Simulink/Stateflow. J. Comput. Sci. Technol. 35 (6) (2020)
Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. ARCH (2020)
Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan
PAC Learning of Deterministic One-Clock Timed Automata. ICFEM (2020)
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning One-Clock Timed Automata. TACAS (1) (2020)
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning One-Clock Timed Automata. CoRR (2019)
Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun
Design of Point-and-Click User Interfaces for Proof Assistants. ICFEM (2019)
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ARCH@CPSIoTWeek (2019)
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
NIL: Learning Nonlinear Interpolants. CoRR (2019)
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
NIL: Learning Nonlinear Interpolants. CADE (2019)
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. CAV (2) (2019)
Bohua Zhan
holpy: Interactive Theorem Proving in Python. CoRR (2019)
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
Quantum Hoare Logic. Arch. Formal Proofs 2019 (2019)
Fabian Immler, Bohua Zhan
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. CPP (2019)
Bohua Zhan
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. J. Autom. Reason. 63 (2) (2019)
Bohua Zhan
Efficient Verification of Imperative Programs Using Auto2. TACAS (1) (2018)
Bohua Zhan, Maximilian P. L. Haslbeck
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. IJCAR (2018)
Bohua Zhan
Auto2 Prover. Arch. Formal Proofs 2018 (2018)
Bohua Zhan, Maximilian P. L. Haslbeck
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. CoRR (2018)
Fabian Immler, Bohua Zhan
Smooth Manifolds. Arch. Formal Proofs 2018 (2018)
Bohua Zhan
Verifying Imperative Programs using Auto2. Arch. Formal Proofs 2018 (2018)
Bohua Zhan
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. ITP (2017)
Bohua Zhan
Formalization of the fundamental group in untyped set theory using auto2. CoRR (2017)
Bohua Zhan
AUTO2, a saturation-based heuristic prover for higher-order logic. CoRR (2016)
Bohua Zhan
AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. ITP (2016)
Bohua Zhan
Automation of separation logic using auto2. CoRR (2016)
Bohua Zhan, Shelby Kimmel, Avinatan Hassidim
Super-polynomial quantum speed-ups for boolean evaluation trees with hidden structure. ITCS (2012)