学术成绩：
　　（1） 高效能符号计算与自动推理算法
　　 (1.1) 基于布尔多项式余式计算的定理自动证明
　　 (1.2) 非经典逻辑框架下自动推理的代数化方法
　　 (1.3) 代数簇分解算法的优化策略及其在几何定理机器证明中的应用
　　 (1.4) 半群非线性命题的多项式时间判定算法
　　（2） 逻辑程序及推理数据库计算语义
　　 (2.1) 对称约简与逻辑程序和推理数据库的计算语义拓广
　　 (2.2) 多项式结构应用于非经典逻辑程序的程序设计方法论
　　（3） 高可信复杂并发系统形式化设计与验证分析
　　 (3.1) 语言和结构层次上功能行为与性能指标混合的复杂并发系统真并发模型
　　 (3.2) 动作细化与功能行为及性能指标混合并发系统的组合层次化理论
　　 (3.3) 包含非协调信息的复杂并发系统的超协调刻画逻辑体系及模型检测技术
　　 (3.4) 基于符号计算方法的并发系统的刻画与验证评价技术
　　 (3.5) 随机时序逻辑与交互式马尔科夫链的组合层次化理论与模型检测技术
　　 (3.6) 组合层次化理论在电路综合与分析中的应用
　　（3.7） 集成电路设计验证与分析软件平台原型系统
　　
　　国家、省部级科研项目：
　　项目名称 项目来源、批准号或批文号 资助起讫
　　时间：
　　具有数量指标约束的并发系统的动作细化理论 中科院“百人计划” 2001-2004年
　　混合性能模拟的层次化：理论与应用 国家自然科学基金 2004-2006年
　　混合并发模型的动作细化 德国DFG 2002-2004年
　　定理机器证明与自动推理平台 973子课题 2003-2004年
　　集成电路形式验证技术及其平台研发 科技部中小企业创新基金 2005-2006年
　　集成电路形式验证平台开发 中科院西部之光联合学者 2005-2006年
　　吴方法算法芯片的研发及基于吴方法的形式化验证技术 973子课题 2005-2009年
　　集成电路形式验证技术及其平台开发 成都市重大科技项目 2005-2006年
　　 IC验证技术与平台 四川省科技攻关项目 2006-2007年
　　需求验证与管理 973子课题 2007-2011年
　　基于代数符号计算的新型软件形式化验证技术和支持工具 863项目 2007-2009年
　　并发系统验证和评估分析的代数符号化理论 国家自然科学基金 2009-2011年
　　微分半代数程序模型的等价及等价谱系 国家自然科学基金 2010-2012年
　　嵌入式软件验证与评估若干关键问题研究 教育部博士点基金博导类 2010-2011年
　　
　　论著、专利、知识产权：
　　在《中国科学》、《Acta Informatica》、《ISSAC》、《ICFEM》等国内外重要学术刊物和国际会议论文集上发表科研论文110篇，研究报告16篇，出版学术专著3部，获得软件著作权6项，申请专利3项。