形式化方法、交互式定理证明、嵌入式系统建模和验证。

计算机科学与技术

083500-软件工程
081202-计算机软件与理论

形式化方法

2010-09--2014-06   普林斯顿大学   博士学位
2007-09--2010-06   麻省理工学院   学士学位

   

2017-08~2018-07,慕尼黑工业大学, 博士后
2014-09~2017-06,麻省理工学院, 博士后

   

程序理论部分：2019-2020秋季、2020-2021秋季。

   

[1] Huanhuan Sheng, Alexander Bentkamp, 詹博华. HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. FM 2023[J]. 2023, 160-178, [2] Yang, Tengshun, Wang, Shuling, Zhan, Bohua, Zhan, Naijun, Li, Jinghui, Xiang, Shuangqing, Xiang, Zhan, Mao, Bifei. Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). JOURNAL OF SYSTEMS ARCHITECTURE[J]. 2022, 126: http://dx.doi.org/10.1016/j.sysarc.2022.102478.
[3] Jie AN, Lingtai WANG, Bohua ZHAN, Naijun ZHAN, Miaomiao ZHANG. Learning real-time automata. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2021, 64(9): 53-69, [4] Jin, Xiangyu, An, Jie, Zhan, Bohua, Zhan, Naijun, Zhan, Miaomiao. Inferring Switched Nonlinear Dynamical Systems. FORMAL ASPECTS OF COMPUTING[J]. 2021, 33(3): 385-406, http://dx.doi.org/10.1007/s00165-021-00542-7.
[5] Zhan, Bohua, Gu, Bin, Xu, Xiong, Jin, Xiangyu, Wang, Shuling, Xue, Bai, Li, Xiaofeng, Chen, Yao, Yang, Mengfei, Zhan, Naijun. Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. 2021 IEEE 27TH REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2021)[J]. 2021, 457-460, [6] Runqing Xu, Liming Li, Bohua Zhan. Verified interactive computation of definite integrals. International Conference on Automated Deduction[J]. 2021, [7] An, Jie, Zhan, Bohua, Zhan, Naijun, Zhang, Miaomiao. Learning Nondeterministic Real-Time Automata. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS[J]. 2021, 20(5): http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000699999600050.
[8] Lin, QianQian, Wang, ShuLing, Zhan, BoHua, Gu, Bin. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using Uppaal and Simulink/Stateflow. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2020, 35(6): 1324-1342, http://lib.cqvip.com/Qikan/Article/Detail?id=7103652898.
[9] Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS[J]. 2020, 12078: 444-462, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439748/.
[10] Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan. PAC learning of deterministic one-clock timed automata. ICFEM 2020[J]. 2020, [11] Zhan, Bohua. Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. JOURNAL OF AUTOMATED REASONING[J]. 2019, 63(2): 517-538, http://dx.doi.org/10.1007/s10817-018-9478-0.
[12] Fabian Immler, Bohua Zhan. Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. INTERNATIONALCONFERENCEONCERTIFIEDPROGRAMSANDPROOFS[J]. 2019, [13] Liu Junyi, Zhan Bohua, Wang Shuling, Ying Shenggang, Liu Tao, Li Yangjia, Ying Mingsheng, Zhan Naijun. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. COMPUTER AIDED VERIFICATION, CAV 2019, PT II[J]. 2019, 11562: 187-207, [14] Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun. Design of Point-and-Click User Interfaces for Proof Assistants. Formal Methods and Software Engineering[J]. 2019, [15] Chen Mingshuai, Wang Jian, An Jie, Zhan Bohua, Kapur Deepak, Zhan Naijun. NIL: Learning Nonlinear Interpolants. 2019, http://arxiv.org/abs/1905.11625.
[16] Zhan, Bohua, Haslbeck, Maximilian P L. Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. AUTOMATED REASONING, IJCAR 2018[J]. 2018, 10900: 532-548, [17] Zhan, Bohua. AUTO2, a saturation-based heuristic prover for higher-order logic. http://arxiv.org/abs/1605.07577.
[18] Bohua Zhan. Efficient Verification of Imperative Programs Using Auto2. Tools and algorithms for the construction and analysis of systems : Parts I /. 23-40, http://arxiv.org/abs/1610.06996.

   

（ 1 ） ****C类, 主持, 部委级, 2019-01--2020-12

现指导学生

许润清  硕士研究生  081202-计算机软件与理论  

盛欢欢  硕士研究生  081200-计算机科学与技术  

详细信息请见：http://lcs.ios.ac.cn/~bzhan/