国防科技大学教授，CCF 高级会员。主要研究领域为形式化方法、自动机理论、AI算法形式验证等。研究成果发表在TSE、ASE、ICSE、IJCAI等国际期刊/会议上。在TACAS工具验证比赛中多次获得冠军。长期从事形式化方法基础理论的教学，为本科生、研究生讲授《抽象代数》、《数理逻辑》、《计算理论》、《计算机逻辑学》等课程。
