个人简介

　　湖北荆门人。长期从事计算机基础、计算机网络一线教学工作，多次组织和参与信息管理系统、监控系统的研发，先后发表了计算机网络、软件正确性验证等方向多篇论文。

教育背景

　　1992.9-1996.7  中国人民解放军军械工程学院（现陆军工程大学）电子系，雷达工程专业，本科
　　2001.9-2004.7  厦门大学自动化系，数据挖掘方向，硕士
　　2005.9-2010.7  清华大学计算机系，软件形式化验证方向，博士

研究方向

　　主要研究方向为软件形式化验证、自动定理证明和人工智能，先后组织开发了C语言模型检测器、Craig插值自动定理证明器等工具。