姓名：吴尽昭 性别：男 出生年月：1965年10月
职称：副教授 学院：中科院成都计算机应用研究所
研究方向：应用于集成电路、片上多核处理器、轨道列车控制系统的设计与分析
工作和学习经历:
1994年7月于中科院系统科学研究所获理学博士学位(导师：吴文俊院士)，1994年9月至1996年8月在北京大学数学学院从事博士后研究(合作导师：程民德院士),1996年9月起任北京大学数学学院副教授，1997至2005年在德国Max-Planck计算机科学研究所和Mannheim大学计算机科学系任研究员，2001年起任中科院成都计算所研究员、博士生导师。
专业领域及专长：
符号计算、自动推理、逻辑程序设计、复杂并发系统形式化分析与验证及其交叉、融合与应用。
学术兼职：
北京交通大学兼职教授，博士生导师、兰州大学萃英讲席教授、中国数学会计算机代数专业委员会委员、教育部高校教学指导委员会计算机科学与技术分委会委员、国家自然科学奖励评审专家、国家863项目评审专家、教育部留学回国人员科研启动基金评审专家、科技部国际合作项目评审专家、四川省专家评议委员会委员。
荣誉称号：
德国“马普学会奖学金”获得者（1997年），中国科学院“百人计划（国外引入杰出人才）”入选者(2000年)，国家“新世纪百千万人才工程国家级人选”(2004年)，四川省学术和技术带头人(2005年)，国务院政府特殊津贴（2006年）。
教学情况：
离散数学，有限域，代数符号计算，自动推理，计算机科学中的逻辑，可计算性理论，程序语言设计，进程代数，计算机代数，人工智能，并发系统设计与验证。
人才培养： 指导毕业博士生15名，指导在读博士生10名，博士后1名。
学术成绩：
（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项。
代表性著作：
时间：
交互式马尔科夫链-并发系统的设计、验证与评估 科学出版社 2007
进程代数-对称与动作细化 科学出版社 2007
代表性论文：
First-Order Polynomial Based Theorem Proving. Mathematics Mechanization and Applications Academic Press, London, 273 - 294 2000
Green Equivalences and Regular Problem for Special Monoids ISSAC\'93, ACM Press, New York, 78 - 85 1993
An Algebraic Method to Decide the Deduction Problem in Propositional Many-Valued Logics ISMVL\'94, IEEE Computer Society Press 1994
Remainder Method for the First-Order Theorem Proving ASCM\'95, Scientists Incorporated, Japan, 91 – 98 1995
On Theorem Proving Using Generalized Odd-Superposition II Sci. China (Ser. E), 39(6), 608 - 619 1996
Mechanical Geometry Theorem Proving Based on Groebner Bases J. Computer Sci. & Technol., 12(1), 10 - 16 1997
Well-Behaved Inference Rules for First-Order Theorem Proving J. Automated Reasoning, 21(3), 381 - 400 1998
Symmetry and Logic Programming. Proc. 11th Nordic Workshop on Programming Theory Uppsala Uni., Sweden 1999
Linear Strategy for Boolean Ring Based Theorem Proving J. Computer Sci. & Technol., 15(3), 271 - 279 2000
CWA Formalizations in Multi-Valued Logics J. Computer Sci. & Technol., 16(3), 263 - 269 2001
Bundle Event Structures: A Revised Cpo Approach Information Processing Letters, 83, 7 - 12 2002
Towards Action Refinement for True Concurrent Real Time Acta Informatica, 39(8), 531 - 577 2003
Symmetric Structure in Logic Programming J. Computer Sci. & Technol., 19(6), 803 - 811 2004
Action Refinement for Real-Time Concurrent Processes with Urgency J. Computer Sci. & Technol., 20(4),514 - 525 2005
Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity Acta Informatica, 42（6-7）, 389 – 418 2006
Multi-Valued Model Checking via Groebner Basis Approach TASE\'07, 35 – 44, IEEE Computer Society Press 2007
Probabilistic Modal Kleene Algebra and Hoare-Style Logic ICNC’08, 652 - 661, IEEE Computer Society Press 2008
Process Algebra Approach to Verifying Safety Specification of Hybrid Systems ICCSN’09, 129 – 133, IEEE Computer Society Press 2009
Ontology Reasoning and Services Composition Verification towards O-RGPS Requirement Meta-Model ICACTE’10, 273-277, IEEE Computer Society Press 2010
专利：
企业多遗留系统的基础数据交换验证平台 申请号：200810045874.3
企业应用集成平台构建方法和体系结构 申请号：200810045875.8
基于交互式马尔可夫链模型检测的嵌入式系统性能评价技术方案 申请号：200910059677.1
知识产权：
IC验证平台“巨微”系统V1.0 软件著作权，登记号: 2006SR06259
“巨微”集成电路等价验证系统V1.0 软件著作权，登记号: 2007SR00744
“巨微”集成电路形式验证引擎BDD软件V1.0 软件著作权，登记号: 2007SR18598.
“巨微”集成电路形式验证引擎SAT Solver软件V1.0 软件著作权，登记号: 2007SR20184
“基于交互式马尔科夫链的模型检测平台软件. 软件著作权，登记号: 2009SR024924
“代数符号计算模型检测软件 软件著作权，登记号: 2009SR024925
近三年科研计划：
通过符号计算与并发系统设计与分析理论的交叉、融合与应用研究，构建功能行为、性能指标和数据结构三维统一的并发系统（软件/协议/硬件）的验证与评估理论、方法和技术。
联系方式：
Email: himrwujz@yahoo.com.cn