吴尽昭导师简介
主要研究方向：
(1) 形式刻画与验证
(1.1) 进程代数的形式语义
(1.2) 复杂并发系统的组合层次化理论与技术
(1.3) 集成电路形式验证技术及其系统平台开发
(2) 符号计算与自动推理
(2.1) 多项式理想的分解算法及其在几何定理机器证明中的应用
(2.2) Wu-Ritt方法及Groebner基理论
(2.3) 逻辑层次上定理机器证明的代数化
(3) 逻辑程序设计与推理数据库
(3.1) 逻辑程序及推理数据库的代数结构与语义
(3.2) 基于非经典逻辑的程序设计方法
简介：
（一）形式刻画与验证
性能评价是研究和优化大规模复杂系统的个体分支之间的动态性质的一门新兴学科。传统的性能评价模型如排队系统和Petri网模型都不具有组合层次性。我们所从事的功能性能模型的语义及其组合层次化理论与技术的研究是最近十年来在性能评价这一领域一个公认的挑战性问题。该理论的研究是具有前瞻性、创新性的应用基础研究。研究成果不但可以用来有效地控制系统设计的复杂度，而且在系统的刻画与验证领域有着重要应用。能够用来解决工业上的(industrial- size)实际问题，特别对大型复杂软件系统的设计方法论具有指导意义。
目前我们的主要工作是由精化入手，研究混有确定性时间、随机时间以及概率等指标的既能用于功能性分析又能用于性能评估的混合复杂系统的语义及其组合层次化。众所周知，精化是复杂系统组合层次化的核心技术。对于传统的无数量指标的系统，其前沿工作主要由英国Oxford大学、美国Stanford 大学、德国Mannheim 大学和荷兰Twente大学完成。在混合性能评价模型的语义及其组合层次化研究方面，我们与德国Mannheim 大学合作，完成了一系列前沿工作。主要研究成果发表在例如《Acta Informatica》、《Information Processing Letters》以及《LNCS》等国际著名学术刊物上。
众所周知，集成电路设计和制造业是我国发展电子信息产业的龙头，集成电路形式验证方法和技术是国际上正在兴起的IC设计先进技术，随着集成电路设计日趋复杂化，设计的验证工作越发繁重，验证技术已经成为制约我国集成电路产业发展的瓶颈，尽管目前全国有集成电路设计单位数百家，但目前还没有从事对于高端集成电路进行验证的专业工具。因此，不论是从产业化还是从信息安全的角度来看，开发具有我国自主知识产权的验证平台工具都很有必要。
在应用研发方面，我们组织了集成电路形式验证软件平台“巨微(ChipVeri)”的开发工作，目前已完成原型软件的开发并已着手软件产业化前期工作。“巨微”使用了目前国际上最新的形式验证技术。“巨微”的研发，弥补了我国在集成电路验证领域的严重不足。它的进一步开发和完善，对加大和挖掘我国集成电路设计与制造产业的发展潜力，具有巨大的产业价值、科技研究价值和经济价值，必将对我国集成电路产业发展和壮大起到积极的推动作用。
我们在该领域的主要工作归纳如下：
（1）在语言和结构层次上建立了混合性能评价模型；
（2）通过定义精化实现混合系统的真并发语义及其组合层次化；
（3）组合层次化理论特征性质，例如正确性以及语法与语义的关系的研究；
（4）集成电路形式化验证系统平台的研究开发。
（二）符号计算与自动推理
定理机器证明通常是指基于逻辑的定理机器证明。这种自动推理模式具有一般性，既原则上可用来证明所有（数学）定理。但这种普遍适用性导致了实际的不可行性，既效率太低。如何改变这种状况？我们知道，符号计算中的吴方法以及Groebner基理论都是以代数为工具来证明几何定理，虽不具有普遍性，但效率极高。
通过定义布尔多项式来实现逻辑定理机器证明的代数化，我们将吴方法等理论的框架嵌入逻辑定理证明中去，以获得既有普遍性效率又高的方法。另一方面，不同逻辑系统的表达能力不同。我们不但研究经典逻辑上的定理证明，也研究了非经典逻辑，例如多值逻辑与注记逻辑上的定理证明。由于代数簇分解算法在吴方法等符号计算理论中的核心地位，我们还研究这一算法的改进，主要侧重于算法的并行化以及相关的复杂度问题。另一方面，半群作为最基本的代数结构，一直吸引着人们的注意。幺半群的性质判定是我们的另一研究方向。主要研究非线性命题，例如正则性等问题，的可判定性。
我们在这方面的工作主要发表在例如《J. Automated Reasoning》、《中国科学》、《Discrete Math.》以及《ISSAC》等国际著名学术刊物和会议论文集上。
我们在该领域的主要工作归纳如下：
（1） 建立基于布尔多项式的定理机器证明方法；
（2） 非经典逻辑框架下的定理证明；
（3） 代树簇分解算法的改进以及幺半群的性质判定。
（三）逻辑程序设计和推理数据库
语义研究是逻辑程序设计和推理数据库中的一个重要课题。衡量一个给定语义成功与否有三个标准：是否与常识相吻合；表达能力如何；以及是否具有可计算性。用这三个标准衡量，几乎所有已知的逻辑程序语义都有缺陷。
我们充分地意识到了这一问题，通过对逻辑程序中的对称结构的深入研究，首次系统地提出了一种处理逻辑程序语义的方法论，使得语义的表达能力以及可计算性得到加强，同时保持与常识相吻合这一重要性质。
例如，我们定义了一种称为G-CWA的语义来处理否定信息，具有较强的可计算性和表达能力并且是众所周知的GCWA的推广，同时增强了SLD-归结、完全化过程以及标准模型语义的表达能力。我们还定义了三类称为G-确定、G-层次和G-分层的逻辑程序，比确定、层次和分层的程序更加一般，并且在此基础上定义了类似于经典的SLD-归结、SLDNF-归结的操作语义。
把逻辑程序设计中的语义推广应用到非经典逻辑中去，不论在理论上还是在实践中都具有重要意义。我们将用于定理机器证明的吴方法的思想应用了到基于非经典逻辑的程序设计和推理数据库中去，开创性地研究了如何用类似多项式的结构来表达知识，以获得直观自然的非经典逻辑，例如多逻辑的程序语义。
我们在该领域的主要工作归纳如下：
（1）通过对称性的研究拓广逻辑程序和推理数据库的语义；
（2）研究代数结构在非经典逻辑程序设计中的应用。
主要工作经历：
1984.9－1988.7 兰州大学数学系，基础数学，理学学士；
1988.9－1991.7 兰州大学计算机系，计算机软件与理论，理学硕士；
1991.9－1994.7 中科院系统科学研究所，基础数学，理学博士；
1994.8－1996.7 北京大学数学学院，计算机软件与理论，博士后；
1996.7－1996.12 北京大学数学学院，计算机软件与理论，副教授；
1997.1－1998.1 Texas A&M大学信息工程系，计算机软件与理论，研究助理；
1998.1－1999.12 Max-Planck计算机所，计算机软件与理论，研究员；
2000.1－2001.6 Mannheim大学计算机系, 计算机软件与理论，科学雇员；
2001.6－至今 Mannheim大学计算机系，计算机软件与理论，兼职教授；
2001.3－至今 中科院成都计算机应用研究所，计算机软件与理论，研究员；
2002.5－至今 中科院成都计算机研究所，计算机软件与理论，博士生导师；
2004.10－至今 兰州大学信息学院，计算机软件与理论，讲座教授；
2004.10-至今 电子科大光电信息学院，计算机软件与理论，兼职教授；
2003.12－至今 成都集成电路验证工程技术研究中心，主任、首席科学家。
研究成果与获奖情况：
（1）中科院“百人计划（国外引入杰出人才）”入选者；
（2）国家人事部等七部委的“百千万人才工程国家级人选”。
论文选列:
[1]H. Fecher, M. Majster-Cederbaum, and J. Wu. Action Refinement for Probabilistic Processes with True Concurrency Models. Lecture Notes in Computer Science, 2399: 77 - 94, 2002.
[2]H. Fecher, M. Majster-Cederbaum, and J. Wu. Bundle Event Structures: A Revised Cpo Approach. Information Processing Letters, 83: 7 – 12, 2002.
[3]H. Fecher, M. Majster-Cederbaum, and J. Wu. Refinement of Actions in a Real-Time Process Algebra with a True Concurrency Model. Electronic Notes in Theoretical Computer Science, 70(3), 2002.
[4]J. Jiang, J. Wu. The preserving of interleaving equivalences. ICECCS'05, IEEE Computer Society Press, pp.580-589, 2005.
[5]J. Jiang, J. Wu. Symmetry and Autobisimulation. Proceedings of the International Conference on Parallel and Distributed Computing, Applications and Technologies. IEEE Computer Society Press, 2005.
[6]J. Jiang, J. Wu, W. Yan. Structural Reductions in Process Algebra Languages. Proceedings of the Joint International Computer Conference. World Scientific Publishing Co. 2005
[7]M. Lu, J. Wu, On Theorem Proving in Annotated Logics. J. Applied Non-Classical Logics, 10(2), 121 - 143, 2000.
[8]M. Majster-Cederbaum, J. Wu. Towards Action Refinement for True Concurrent Real Time. Acta Informatica, 39(8), 2003.
[9] M. Majster-Cederbaum, J. Wu. Adding Action Refinement to Stochastic True Concurrency Models. Lecture Notes in Computer Science, 2885:226-245, 2003.
[10] M. Majster-Cederbaum, J. Wu. Action Refinement for True Concurrent Real Time. Proc. ICECCS ‘01, IEEE Computer Society Press, 58 - 68, 2001.
[11] Mila Majster-Cederbaum, Jinzhao Wu, Houguang Yue and Naijun Zhan. Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. ICFEM04, Lecture Notes in Computer Science, 3308:449-463, 2004.
[12] M. Majster-Cederbaum, J. Wu and H. Yue. Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity (full version). Accepted by Acta Informatica, 2005 .
[13] W. Mao, J. Wu. Application of Wu's method to symbolic model checking. ISSAC'05, ACM Press, pp. 237-244, 2005.
[14]W. Mao, X. Sun, D. Chen, J. Wu. Design of a No Reference Counting Field BDD Package. Journal of Computer Applications, Vol.16, No.10, pp. 35-37, 2004.
[15] G. Qin and J. Wu. Branching Time Equivalences for Interactive Markov Chains. Lecture Notes in Computer Science, 3236: 156-169, Dec. 2004.
[16] G. Qin and J. Wu. Action Refinement for Real-Time Concurrent Processes with Urgency. ARTS’04, ENTCS, 2004.
[17] G. Qin and J. Wu. Action Refinement for Real-Time Concurrent Processes with Urgency. Journal of Computer Science and Technology, 20( 4): 514-525, 2005.
[18] X. Sun, J. Wu, X. Song and M. Majster-Cederbaum. Formal specification of an asynchronous processor via action refinement. 5th International Workshop on Microprocessor Test and Verification, IEEE Computer Society Press, pp. 142-148, 2004.
[19] X. Sun, W. Zhang and J. Wu. Event-Based Operational Semantics and a Consistency Result for Real-Time Concurrent Processes with Action Refinement. Journal of Computer Science and Technology. 19(4): 828-839, 2004.
[20] X. Sun, J. Wu. Operational semantics for real-time processes with action refinement. Proc. SEFM 2005, IEEE Computer Society Press, pp. 54-63, 2005.
[21] J. Wu and H. Yue. Towards Action Refinement for Concurrent Systems with Causal Ambiguity. Proc. SEFM 2004, IEEE Computer Society Press, 300-309, 2004.
[22]J. Wu and H. Yue. Towards Action Refinement for Concurrent Systems with Causal Ambiguity. SEFM’04, IEEE Computer Society Press, pp. 300-309, 2004.
[23]J. Wu, W. Zhang, Z. Zeng. Automatic Generation of Mathematical Expression of Printed Chinese Character. The Fourth IASTED International Conference on Computational Intelligence, pp. 123-126, 2005 .
[24]J. Wu, H. Fecher. Symmetric Structure in Logic Programming, Journal of Computer Science and Technology. 19(4):803-811, 2004.
[25]J. Wu. CWA Extensions to Multi-Valued Logics. J. Applied Non-Classical Logics, 2003.
[26]J. Wu. Symmetry and Logic Programming. Proc. 32 JAIIO - WAIT'03, Argentinian Workshop on Theoretical Computer Science, 2003.
[27]J. Wu, CWA Formalizations in Multi-Valued Logics. J. Computer Sci. & Technol., 16(3), 263 - 269, 2001.
[28]J. Wu. Action Refinement in Timed LOTOS. Proc. of ASCM, World Scientific Publ., 183 - 192, 2001
[29]J. Wu, First-Order Polynomial Based Theorem Proving. Mathematics Mechanization and Applications, Academic Press, London, 273 - 294, 2000.
[30]J. Wu, Linear Strategy for Boolean Ring Based Theorem Proving. J. Computer Sci. & Technol., 15(3), 271 - 279, 2000.
[31]J. Wu, Logic Programming -- Taking Advantage of Symmetry. Proc. of ASCM, World Scientific Publ., 100 - 109, 2000.
[32]J. Wu, Symmetry and Logic Programming . Proc.11th Nordic Workshop on rogramming Theory, Sweden, 1999.
[33]J. Wu, Well-Behaved Inference Rules for First-Order Theorem Proving. J. Automated Reasoning, 21(3), 381 – 400，1998.
[34]J. Wu, An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics. J. Applied Non-Classical Logics, 8(4), 353-360, 1998.
[35]J. Wu, Extending CWA to Multi-Valued Logics. Proc. of ASCM, Lanzhou Univ. Press, 259 - 271, 1998.
[36] J. Wu, Mechanical Geometry Theorem Proving Based on Groebner Bases. J. Computer Sci. & Technol., 12(1), 10-16, 1997.
[37] J. Wu, Linear Strategy, Semantic Strategy and Lock Strategy in Remainder Method. Chinese J. Computer, 20(2), 1997.
[38] J. Wu, An Algorithm for Decomposing Zero- Dimensional Ideals. J. of Math., 17(4), 450 - 454, 1997.
[39] J. Wu, Quantitative Properties of Green Equivalences for Special Monoids. J. Sys. Sci. & Math. Sci., 9(3), 198-204, 1996.
[40] J. Wu, On Algebraic Variety Decomposition. J. Sys. Sci. & Math. Sci., 9(2), 120-127, 1996.
[41] J. Wu, On Theorem Proving using Generalized Odd-Superposition II. Sci. China (Ser. E), 39(6), 608-619, 1996.
[42]J. Wu, A Method for Automated Geometry Theorem Proving. J. Sys. Sci. & Math. Sci., 9(4), 313-319, 1996.
[43]J. Wu, Remainder Method for the Mechanical Theorem Proving in First-Order Predicate Calculus (in Chinese). Chinese J. Computer, 19(10), 728 - 734, 1996.
[44]J. Wu, Two Properties of Special Monoids. Acta Mathematica Sinica, 39(4), 1996.
[45]J. Wu, On First-Order Theorem Proving. Proc. of ASCM, Scientists Incorporated, Japan, 163 - 168, 1996.
[46]J. Wu, Mechanical Theorem Proving in Many-Valued Logics. Chinese J. Computer, 19(10), 773 - 779, 1996.
[47]J. Wu, Remainder Method for the First-Order Theorem Proving. Proc. of ASCM, Scientists Incorporated, Japan, 91 - 98, 1995.
[48]J. Wu, A Zero-Dimensional Method for Geometry Theorem Proving. J. of Mathematical Research and Exposition, 15(4), 617 - 632, 1995.
[49]J. Wu, An Algebraic Method to Decide the Deduction Problem in Propositional. Proc. of ISMVL, IEEE Computer Society Press, 1994.
[50]J. Wu, Green Equivalences and Regular Problem for Special Monoids. Proc. of ISSAC, ACM Press, New York, 78-85, 1993.
联系方式:
Email:
Wu@pil.informatik.uni-mannheim.de
Tel: 028-85249933-8411
