本科部 中国科学院大学本科教育网

本人主要工作领域为形式化方法，特别是概率或并发系统、软硬件系统的建模与正确性检验。本人不但关注系统的形式验证的理论研究工作，同时也注重验证工具的开发：曾经一起带领成功开发带参数的检验工具（PARAM）、基于反例的模型检验工具（PASS）、概率混成系统模型检测工具（ProHVer）等（参见工具网页iscasmc.ios.ac.cn）。本人致力于将其用到网络协议的分析、分布并发式系统的建模与检验中去。