基本信息
詹博华  男  硕导  中国科学院软件研究所
电子邮件: bzhan@ios.ac.cn
通信地址: 中国科学院软件所
邮政编码:

研究领域

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

招生信息

计算机科学与技术

招生专业
083500-软件工程
081202-计算机软件与理论
招生方向
形式化方法

教育背景

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

工作经历

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

教授课程

   
数理逻辑和程序理论

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

出版信息

   
发表论文
[1] 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). Journal of Systems Architecture. 2022, 126: [2] Jie AN, Lingtai WANG, Bohua ZHAN, Naijun ZHAN, Miaomiao ZHANG. Learning real-time automata. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2021, 64(9): 53-69, [3] 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.
[4] 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, [5] Runqing Xu, Liming Li, Bohua Zhan. Verified interactive computation of definite integrals. International Conference on Automated Deduction[J]. 2021, [6] 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.
[7] 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.
[8] 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/.
[9] Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan. PAC learning of deterministic one-clock timed automata. ICFEM 2020[J]. 2020, [10] Zhan, Bohua. Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. JOURNAL OF AUTOMATED REASONING[J]. 2019, 63(2): 517-538, https://www.webofscience.com/wos/woscc/full-record/WOS:000475656400016.
[11] Fabian Immler, Bohua Zhan. Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. International Conference on Certified Programs and Proofs[J]. 2019, [12] 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, [13] Chen Mingshuai, Wang Jian, An Jie, Zhan Bohua, Kapur Deepak, Zhan Naijun. NIL: Learning Nonlinear Interpolants. 2019, http://arxiv.org/abs/1905.11625.
[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] Zhan, Bohua, Haslbeck, Maximilian P L. Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. AUTOMATED REASONING, IJCAR 2018[J]. 2018, 10900: 532-548, [16] Zhan, Bohua. AUTO2, a saturation-based heuristic prover for higher-order logic. http://arxiv.org/abs/1605.07577.
[17] 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/