男，博士，现为北京大学信息科学技术学院教授，软件研究所副所长。主要研究领域为程序理论，研究方向包括程序逻辑，程序语义，分布式系统的描述与验证。多年主讲北京大学信息科学技术学院本科生离散数学课程和研究生形式语义课程，此外讲授过高等数学、形式化方法等多门课程。教育部师资培训离散数学课程主讲教师。已在国际会议、国内外学术杂志上发表论文60余篇，教材或译著7部。主持或参加国家自然科学基金项目、863项目、973项目等10余项，参与建设的离散数学课程体系建设在2001年评为北京市教学成果奖一等奖，获教育部高等学校科学技术奖励自然科学一等奖（排名2/5，2011），北京大学杨芙清王阳元院士优秀教学科研奖（2010年），日本大川研究助成奖（Research Grant）(日本大川情报通信基金会，1/1，2006), 中国人工智能学会离散数学专业委员会副主任委员。