个人简介
湖北荆门人。长期从事计算机基础、计算机网络一线教学工作，多次组织和参与信息管理系统、监控系统的研发，先后发表了计算机网络、软件正确性验证等方向多篇论文。
教育背景
1992.9-1996.7 中国人民解放军军械工程学院（现陆军工程大学）电子系，雷达工程专业，本科
2001.9-2004.7 厦门大学自动化系，数据挖掘方向，硕士
2005.9-2010.7 清华大学计算机系，软件形式化验证方向，博士
研究方向
主要研究方向为软件形式化验证、自动定理证明和人工智能，先后组织开发了C语言模型检测器、Craig插值自动定理证明器等工具。