逻辑方法；程序正确性方法；

   

081202-计算机软件与理论

并发系统分析与验证

   

1978：北京大学数学系
1979：挪威奥斯陆大学语言培训班
1980-1988：挪威奥斯陆大学计算机系

1988：博士学位

2001年中国科学院软件研究所研究员。主要从事逻辑方法与程序正确性方法研究。

获2008年首届中国科学院“朱李月华优秀教师奖”。

   

[1] 张文辉, 高雅. A Bounded Semantics for Improving the Efficiency of Bounded Model Checking. 26th International Conference on Engineering of Complex Computer Systemsnull. 2022, [2] 包玉龙, 朱雪阳, 张文辉, 沈武威, 孙鹏飞, 赵颖琪. On Verification of Smart Contracts via Model Checking. The 16th International Symposium on Theoretical Aspects of Software Engineeringnull. 2022, [3] Zhang, Wenhui, Zhu, XueYang, Bao, YuLong, IEEE COMP SOC. VERDS: Modeling and Verification of Finite State Systems with Discrete Time Models by Symbolic Techniques. 2021 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2021)null. 2021, 135-142, [4] Chen Ran, Zhang Wenhui, IEEE. Verification of CTLBDI Properties by Symbolic Model Checking. 2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC)null. 2019, 102-109, [5] Jian Zhang. Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring. The 28th International Joint Conference on Artificial Intelligence. 2019, [6] Chen, Ran, Zhang, Wenhui, IEEE Comp Soc. Checking Multi-Agent Systems against Temporal-Epistemic Specifications. 2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019)null. 2019, 21-30, http://dx.doi.org/10.1109/ICECCS.2019.00010.
[7] Liu, Xinxin, Yu, Tingting, Zhang, Wenhui, Baier, C, Lago, UD. Logics for Bisimulation and Divergence. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2018null. 2018, 10803: 221-237, [8] Wenhui Zhang. Characterization and Verification of Stuttering Equivalence. LNCS 11180 (Symposium on Real-Time and Hybrid Systems 2017). 2018, [9] Xu, Zhaowei, Zhang, Wenhui, Sui, Yuefei, Steffen, B, Baier, C, VanDenBrand, M, Eder, J, Hinchey, M, Margaria, T. Completeness of Hoare Logic Relative to the Standard Model. SOFSEM 2017: THEORY AND PRACTICE OF COMPUTER SCIENCEnull. 2017, 10139: 119-131, [10] Xu, Zhaowei, Zhang, Wenhui. Linear templates of ACTL formulas with an application to SAT-based verification. INFORMATION PROCESSING LETTERS[J]. 2017, 127: 6-16, http://dx.doi.org/10.1016/j.ipl.2017.06.008.
[11] Liu Xinxin, Yu Tingting, Zhang Wenhui. Analyzing Divergence in Bisimulation Semantics. ACM SIGPLAN NOTICESnull. 2017, 52(1): 735-747, [12] Xu, Zhaowei, Sui, Yuefei, Zhang, Wenhui. Completeness of Hoare logic with inputs over the standard model. THEORETICAL COMPUTER SCIENCE[J]. 2016, 612: 23-28, http://dx.doi.org/10.1016/j.tcs.2015.08.004.
[13] Long, Teng, Zhang, Wenhui. Termination analysis with recursive calling graphs. JOURNAL OF NETWORK AND COMPUTER APPLICATIONS[J]. 2016, 59: 109-116, http://dx.doi.org/10.1016/j.jnca.2015.06.019.
[14] Zhang, Wenhui. Bounded semantics. THEORETICAL COMPUTER SCIENCE[J]. 2015, 564: 1-29, http://dx.doi.org/10.1016/j.tcs.2014.10.026.
[15] Xu Yanyan, Chen Wei, Su Kaile, Zhang Wenhui. Greedy clique decomposition for symbolic satisfiability solving. International Journal of Advancements in Computing Technology[J]. 2012, 4(10): 174-184, http://ir.iscas.ac.cn/handle/311060/15450.
[16] Chen, Wei, Zhang, Wenhui. A direct construction of polynomial-size OBDD proof of pigeon hole problem. INFORMATION PROCESSING LETTERS[J]. 2009, 109(10): 472-477, http://www.corc.org.cn/handle/1471x/2400757.
[17] Wang, XiangYun, Zhang, Wenhui, Li, YongChao, Cai, KaiYuan. A polynomial dynamic system approach to software design for attractivity requirement. INFORMATION SCIENCES[J]. 2007, 177(13): 2712-2725, http://dx.doi.org/10.1016/j.ins.2007.01.025.
[18] Wenhui Zhang. Depth of proofs, depth of cut-formulas and complexity of cut formulas. Theoretical Computer Science. 1996, [19] ZHANG, WH. CUT ELIMINATION AND AUTOMATIC PROOF PROCEDURES. THEORETICAL COMPUTER SCIENCE[J]. 1991, 91(2): 265-284, http://dx.doi.org/10.1016/0304-3975(91)90086-H.

已指导学生

易锦  博士研究生  081202-计算机软件与理论  

黄洪涛  博士研究生  081202-计算机软件与理论  

吴志林  博士研究生  081202-计算机软件与理论  

王绍春  硕士研究生  081202-计算机软件与理论  

徐艳艳  博士研究生  081202-计算机软件与理论  

周翔  博士研究生  081202-计算机软件与理论  

杜金秀  硕士研究生  081202-计算机软件与理论  

徐亮  博士研究生  081202-计算机软件与理论  

陈伟  博士研究生  081202-计算机软件与理论  

李伟松  硕士研究生  081202-计算机软件与理论  

王晓亮  硕士研究生  081202-计算机软件与理论  

冯庆奎  硕士研究生  081202-计算机软件与理论  

龙腾  博士研究生  081202-计算机软件与理论  

张兰兰  硕士研究生  081202-计算机软件与理论  

曾奶举  博士研究生  081202-计算机软件与理论  

现指导学生

许兆伟  博士研究生  081202-计算机软件与理论  

麻婧  硕士研究生  081202-计算机软件与理论  

陈然  博士研究生  081202-计算机软件与理论