Bohua Zhan - RankMe

74 papers A 7B 10C 3Misc 3Journal 40Unranked 10

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