| 词条 | 吴尽昭 |
| 释义 | 吴尽昭，男，汉族，1965年10月出生，中共党员，教授，现任广西民族大学副校长，中科院成都信息技术有限公司研究员，计算机科学家与数学家。 人物简介北京交通大学、中科院成都计算所博士生导师；教育部高校教学指导委员会计算机科学与技术分委会委员、中国数学会计算机代数专业委员会委员、四川省专家评议委员会委员、国家自然科学奖励评审专家、科技部863及国际合作项目评审专家、教育部留学归国人员科研基金评审专家；1994年于中科院系统科学研究所获理学博士学位，1994年至1996年北京大学博士后，1997至2005年就职于德国Max-Planck计算所和Mannheim大学计算机系；2001年起任中科院成都计算所研究员、博士生导师，IC验证工程中心主任；2007年任北京交通大学教授、计算机软件与理论博士生导师；2009年9月任广西民族大学副校长。 长期从事高效能高可信计算与推理理论与工具的研究和开发，研究领域涉及符号计算、自动推理、形式化方法及其交叉、融合与应用；在国内外学术刊物和国际会议论文集上发表研究论文103篇，出版专著3部，获得软件著作权6项，申请专利3项；近年来承担国家自然科学基金、863、973子课题等国家、省部级科研项目10余项，至2009年指导毕业博士研究生14名；1997年获德国“马普学会奖学金”，2000年入选中科院“百人计划(国外引入杰出人才)”，2004年国家“新世纪百千万人才工程国家级人选”，2005年“四川省学术和技术带头人”，2006年获国务院政府特殊津贴专家。 主要经历1991.09－1994.07 中科院系统科学研究所，理学博士 1994.08－1996.07 北京大学数学学院信息科学系，博士后 1996.07－1996.12 北京大学数学学院信息科学系，副教授 1997.01－1998.01 美国Texas A&M大学电子工程系，研究助理 1998.01－1999.12 德国Max-Planck计算机科学研究所，研究员 2000.01－2005.12 德国Mannheim大学计算机科学系，科学雇员/客座教授 2001.04－2006.07 中科院成都计算机应用研究所，研究员/博士生导师 2006.07－2007.07 电子科技大学，教授/博士生导师 2007.07—2009.09 北京交通大学，教授/博士生导师 2009.09—至今 广西民族大学副校长 社会职务兰州大学萃英讲席教授 电子科技大学兼职教授 中国数学会计算机数学专业委员会委员 国家863项目评审专家 教育部留学回国人员科研启动基金评审专家 成都巨微集成电路验证工程技术有限责任公司董事长 北京交通大学教授，计算机软件与理论博士生导师 广西民族大学副校长，主管学科建设与对外交流 研究方向计算机软件与理论 主持项目情况（1） 具有数量指标约束的并发系统的动作细化理论（中科院“百人计划”，2001-2004年，主持） （2） 混合性能模拟的层次化：理论与应用（国家自然科学基金，2004-2006年，主持） （3） 混合并发模型的动作细化（德国DFG，2002-2004年，联合主持） （4） 定理机器证明与自动推理平台（973，2003-2004年，子课题承担人） （5） 偏序时序逻辑及其模型检测（德国DFG，2004-2005年，联合主持） （6） 软件开发与形式化方法（四川省外专局国际合作项目，2004-2005年，主持） （7） 集成电路形式验证技术及其软件平台“巨微”系统的研发（国家科技部中小企业创新基金，2005-2006年，主持） （8） 集成电路形式验证平台开发（中科院西部之光联合学者，2005-2006年，主研） （9） 吴方法算法芯片的研发以及基于吴方法的形式化验证技术（973，2005-2009年，子课题承担人） （10） 集成电路形式验证技术及其平台开发（成都市重大科技项目， 2005-2006年，主持） （11） IC验证技术与平台（四川省科技攻关项目，2006-2007年，主持） （12） 需求形式化验证与评价（973，2007-2010年，子课题承担人） （13） 基于代数符号计算的新型软件形式化验证技术和支持工具（863，2008-2009年，主持） （14） “中科巨微”国产化集成电路设计验证产业化（四川省发改委，2008-2009年，主持） （15） 集成电路验证技术及平台（成都市科技局， 2008-2009年，主持） 主要论著[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. 专著： 1 《交互式马尔可夫链——并发系统的设计、验证与评价》，吴尽昭，王永祥，覃广平著。北京，科学出版社，2007。 2 《进程代数——对称与动作细化》，王永祥，吴尽昭，蒋健民著。北京，科学出版社，2007。 所得荣誉（1）德国“马普学会奖学金”（1997年） （2）中国科学院“百人计划（国外引入杰出人才）”入选者(2000年) （3）国家首批“百千万人才工程国家级人选”(2004年) （4）四川省学术和技术带头人(2005年) （5）国务院政府特殊津贴（2006年） 学术血统/Academy Genealogy吴尽昭(Jinzhao Wu), Ph.D., 1994 中国科学院系统科学研究所（Institute of Systems Science, AMSS, CAS） 吴文俊(Wen-Tsün Wu), Docteur d'Etat, 1949 Université Louis Pasteur - Strasbourg I 查尔斯·埃里斯曼(Charles Ehresmann), Docteur d'Etat, 1934 École Normale Supérieure Paris 埃利·嘉当(Élie Cartan), Ph.D., 1894 Université de Paris 吉恩·加斯顿·达布(Jean Gaston Darboux), Ph.D., 1866 École Normale Supérieure Paris 米奇尔·沙勒(Michel Chasles), Ph.D., 1814 École Polytechnique 西蒙·丹尼斯·泊松(Simeon Denis Poisson), Ph.D., 1800? École Polytechnique 约瑟夫·路易斯·拉格朗日(Joseph Louis Lagrange), no degree, - - 莱昂哈德·欧拉(Leonhard Euler), Ph.D., 1726 Universität Basel 约翰·伯努利(Johann Bernoulli), Dr. med., 1694 Universität Basel 雅格布·伯努利(Jacob Bernoulli), Dr. hab. Sci., 1684 Universität Basel 戈特弗里德·威廉·莱布尼茨(Gottfried Wilhelm Leibniz), Dr. jur., 1666 Universität Altdorf 埃尔哈德·魏格尔(Erhard Weigel), Ph.D., 1650 Universität Leipzig |
| 随便看 |
百科全书收录4421916条中文百科知识，基本涵盖了大多数领域的百科知识，是一部内容开放、自由的电子版百科全书。