出自计算机科学国家重点实验室

职称:	研究员
研究方向：	模型检测与定理证明
电话:	010-62661620
E-Mail:	zwh(at)ios.ac.cn
个人主页：	http://lcs.ios.ac.cn/~zwh/

2001年应聘“百人计划”到实验室工作。主要从事形式化方法及并发系统的形式验证方法与技术方面的研究。在程序验证方面，曾参与针对XYZ语言的时序逻辑推理系统和时序逻辑程序验证方法的研究；在命题逻辑方面，提出了一个分析命题逻辑公式模型个数的算法和是否存在模型的判定算法，推进了命题逻辑公式判定算法的研究；在谓词逻辑推理方面，对引理的使用做了深入的研究，取得了系统性的理论结果；在模型检测方面，将模型检测方法应用于操作程序的验证，提出多种针对具体应用做抽象和分不同情况以降低模型检测空间和时间复杂性的方法；在软件系统设计方法的形式化方面，参与了针对UML系统建模语言部分内容的形式化的研究，并将其应用于分布式系统的设计。