北京交通大學(xué)

基本信息

姓名：吳盡昭

電子郵件：himrwujzh@aliyun.com

教育背景

1991.09-1994.07 中科院系統(tǒng)科學(xué)研究所,理學(xué)博士 1994.08-1996.07 北京大學(xué)數(shù)學(xué)學(xué)院信息科學(xué)系,博士后 1996.07-1996.12 北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院信息科學(xué)系,副教授 1997.01-1998.01 美國(guó)Texas A&M大學(xué)電子工程系,副研究員 1998.01-1999.12 德國(guó)Max-Planck計(jì)算機(jī)科學(xué)研究所,研究員 2000.01-2005.12 德國(guó)Mannheim大學(xué)計(jì)算機(jī)科學(xué)系,研究員 2001.06-2007.10 中科院成都計(jì)算機(jī)應(yīng)用研究所,研究員、博士生導(dǎo)師 2007.10-2009.09 北京交通大學(xué)計(jì)算機(jī)學(xué)院,教授、博士生導(dǎo)師 2009.10- 廣西民族大學(xué),教授、副校長(zhǎng)

科研項(xiàng)目

北京交通大學(xué)：混雜系統(tǒng)的近似等價(jià)及等價(jià)譜系研究，2013-01-01--2014-12-31，40.0萬(wàn)元，主持;博士點(diǎn)基金：嵌入式軟件設(shè)計(jì)驗(yàn)證與評(píng)估若干關(guān)鍵問(wèn)題研究，2010-01-01--2012-12-31，6.0萬(wàn)元，主持;國(guó)家自然科學(xué)基金“面上”：微分半代數(shù)程序模型的等價(jià)及等價(jià)譜系，2010-01-01--2012-12-31，32.0萬(wàn)元，主持;博士點(diǎn)基金：Web服務(wù)組裝中增量及聲明式事務(wù)管理機(jī)制研究，2009-01-01--2011-12-31，3.6萬(wàn)元，參加;國(guó)家自然科學(xué)基金“面上”：復(fù)雜并發(fā)系統(tǒng)驗(yàn)證和評(píng)估分析的代數(shù)符號(hào)化理論與方法，2009-01-01--2011-12-31，35.0萬(wàn)元，主持;�？萍蓟�金：基于代數(shù)符號(hào)計(jì)算的復(fù)雜并發(fā)系統(tǒng)形式化驗(yàn)證技術(shù)，2008-01-01--2010-12-31，10.0萬(wàn)元，主持;片上多核處理器高層次架構(gòu)設(shè)計(jì)的驗(yàn)證理論與關(guān)鍵技術(shù)(廣西自然科學(xué)基金創(chuàng)新研究團(tuán)隊(duì)項(xiàng)目，2012-2014年，200萬(wàn)元，主持);大規(guī)模集成電路高層次設(shè)計(jì)驗(yàn)證技術(shù)(廣西教育廳資助項(xiàng)目，300萬(wàn)元，2011-2014年，主持);近似形式化方法—實(shí)微分多項(xiàng)式進(jìn)程代數(shù)研究(國(guó)家自然科學(xué)基金，2014-2017年， 62萬(wàn)元，主持);......

教學(xué)工作

進(jìn)程代數(shù);模型檢測(cè);計(jì)算機(jī)科學(xué)中的邏輯;人工智能。

論文/期刊

書(shū)籍章節(jié) [1] J. Wu. First-Order Polynomial Based Theorem Proving. Mathematics Mechanization and Applications, Academic Press, London, 273 - 294, 2000. 編輯出版 [1] J. Wu, H. Yi. Proceedings 2010 International Conference on Computer and Computational Intelligence (Volume 1 – 4), IEEE, 2010. [2] J. Wu. Complexity Science. Journal of the University of Electronic Science and Technology of China, 2010 - Present. 期刊論文(英文) [1] Chao Wang, JinZhao Wu, Shuo Yan. Approximation on Polynomial Flow Event Structures in Programs with Singleton Failures Semantics. Journal of Computational Information Systems, to appear, February 2014. [2] Wang Chao, Liang Yi, Wu Jinzhao, Tan Hongyan. Approximate Failures Semantics for Polynomial Labelled Transition Systems. J. EastChina Univ., to appear, 2014. [3] Chao Wang, JinZhao Wu, HongYan Tan. Approximate Bisimulation Functions for First-order Ordinary Differential Systems. Journal of Computational Information Systems, to appear, March 2014. [4] Weidong Tang, Jinzhao Wu and Dingwei Zheng.On Fuzzy Rough Sets and Their Topological Structures. Mathematicial Problems in Engineering, to appear, 2014. [5] Hui Deng, Jinzhao Wu. Approximate Bisimualtion and Optimization of Software Programs Based on Symbolic-Numeric Computation. Mathematical Problems in Engineering, vol.2013, Article ID 421926, 2013. [6] Hui Deng, Jinzhao Wu, Hongyan Tan. Approximate Bisimulation for High-level Datapaths in Intelligent Trtation Systems. Advances in Mechnical Engineering, Vol. 2013, Article ID 305636, 2013. [7] Xinyan Gao, Ning Zhou, Jinzhao Wu, Dakui Li. Wu's Characteristic Set Method for SystemVerilog Assertions Verification. Journal of Applied Mathematics, Volume 2013, Article ID 740194, 2013. [8] Hao Yang, Jinzhao Wu, Zhiwei Zhang, Yang Liu. Approximate Completed Trace Equivalence of Three Dimensional t-Model Nonlinear Algebraic Hybrid Systems. Applied Mathematics & Information Sciences, 7(5), 1693-1697, 2013. [9] Y. Liu, J. Wu. Consistency Verification between Goal Model and Process Model in Requirement Analysis of Networked Software. Journal of Computational and Theoretical Nanoscience, Accepted, 2013. [10] Y. Liu, J. Wu, R. Qiao. Dynamic Evolution of Requirements Process Model Deployed on Network Environment with PZN. Journal of Computational Information Systems, 9(8), 3329-3336, 2013. [11] Y. Liu, J. Wu, R. Zhao. Formal Verification of Process Layer with Petri Net and Z. Advances in Information Sciences and Service Sciences, 5(1), 68-77, 2013. [12] Y. Liu, J. Wu. Dynamic Evolution of Requirements Goal Deployed on Network Environment. International Journal of Innovations in Information Technology, 1(1), 45-48, 2013. [13] Anping He, Jinzhao Wu, Shihan Yang, Yongquan Zhou, Juan Wang. Automata-Based Analysis of Stage Suspended Boom Systems. Journal of Applied Mathematics, Volume 2013, Article ID 739253, 2013. [14] Ning Zhou, Jinzhao Wu, Xinyan Gao. Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches. Journal of Applied Mathematics, Volume 2013, Article ID 272781, 2013. [15] Jiantao Zhou, Jing Liu, Jinzhao Wu, Guodong Zhong. A Latent Implementation Error Detection Method for Software Validation, Journal of Applied Mathematics, Volume 2013, Article ID 138287, 2013. [16] Shihan Yang, Jinzhao Wu, Anping He, Yunbo Rao. Derivation of OWL Ontology from XML Documents by Formal Semantic Modeling. Journal of Computers, 8(2), 372-379, 2013. [17] Yong Huang, Jinzhao Wu. Research on Virtual Network Mapping Algorithm with Path Splitting Based on Sort Preprocessing. J. Computers, 8(9): 2413-2420, 2013. [18] Hui Deng, Jinzhao Wu. Approximate Bisimulation and Its Applications for Polynomial Algebraic System Based on Symbolic and Numerical Calculation. Journal of Information and Computational Science, 9(11), 2012. [19] Hao Yang, Jinzhao Wu, Zhiwei Zhang. Approximate Completed Trace Equivalence of Inhomogeneous Linear Transition Systems. International Journal of Advancements in Computing Technology, 4(8), 58-66, 2012. [20] Bai Liu, Jinzhao Wu. A Clustering Analysis Method Based on Population Migration Algorithm. Journal of Computational Information Systems, 8(9), 3947-3953, 2012. [21] Ning Zhou, Xinyan Gao, Jinzhao Wu. Applying Wu’s Method to Symbolic Simulation for Boolean Layer PSL Assertion Checking. Journal of Convergence Information Technology, 7(4), 272-279, 2012. [22] Yang Liu, Jinzhao Wu. Requirement Verification of Networked Software Goals with Multi-valued Logic. International Journal of Advancements in Computing Technology, 4(20), 301–309, 2012. [23] Weidong Tang, Bai Liu, Chaoqun Zhang, Jinzhao Wu. Study of Mobile Node Localization Algorithm Based on Ranging MCL for WSN. American Journal of Engineering and Technology Research, 11(12), 913-917, 2011. [24] Anping He, William N.N. Hung, Guowu Yang, Jinzhao Wu, Lian Li. Mathematical Analysis of Stage-Based Programmable Logic Controller. Computers & Mathematics with Applications, Volume 61, 1769-1785, 2011. [25] Hui Deng, Jinzhao Wu, Ning Zhou. Approximate Equivalence and Optimization for High-level Datapath. Journal of Computational Information Systems, 8(16)，4131-4142, 2011. [26] Guang Zheng, Jinzhao Wu, Aiping Lu. Stochastic Process Algebra with Value-Passing and Weak Time Restrictions. Journal of Software, 6(5), 769-782, 2011. [27] Liangdong Qu, Dengxu He, Jinzhao Wu. Hybrid Coevolutionary Glowworm Swarm Optimization Algorithm for Fixed Point Equation. Journal of Information and Computational Science, 8(9), 1721-1728, 2011. [28] Liangdong Qu, Dengxu He, Jinzhao Wu. Hybrid Coevolutionary Glowworm Swarm Optimization Algorithm with Simplex Search Method for System of Nonlinear Equations. Journal of Information and Computational Science, 8(13), 2693-2701, 2011. [29] Liangdong Qu, Dengxu He, Jinzhao Wu. Hybrid Coevolutionary Population Migration Algorithm for Integer Programming and Its Application in Neural Network. Journal of Computational Information Systems, 7(11), 3878-3885, 2011. [30] W. Chen, G. Zheng, L. Li, J. Wu. Real Time Process Algebra with Urgency Executing Policy. J. Software, 4(1), 34 - 41, 2009. [31] G. Zheng, L. Li, W. Chen, A. He, J. Wu. Process Algebra with Chaos Executing Policy for Unhealthy Systems. J. Computers, 4(1), 86 - 93, 2009. [32] J. Wu, H. Hou, S. Li. Quasi-Classical Description Logics and Paraconsistent Tabbleau Calculus for Reasoning with Acyclic Tbox. J. Univ. of Electronic Sci. & Tech. Of China, 38(5), 656 – 668, 2009. [33] S. Li, S. Yang, J. Wu. On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-Based System. J. Univ. of Electronic Sci. & Tech. Of China, 38(5), 669 – 677, 2009. [34] X. Sun, F. Xie, J. Wu, X. Song. Verification of a Network ASIC Component Using Bounded Model Checking. International Journal of Electrionics, 94(2), 183 - 196, 2007. [35] M. Majster-Cederbaum, J. Wu, H. Yue. Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. Acta Informatica, 42(6-7), 389 – 418, 2006. [36] J. Jiang, J. Wu. Interleaving and Step Equivalences and Their Preservations under Action Refinement. J. Computer Sci. & Technol., accepted, 2006. [37] G. Yang, X. Song, M. Perkowski, J. Wu. Realizing Ternary Quantum Switching Networks without Ancilla Bits. Journal of Physics A: Mathematical and General, 38, 9689 - 9697, 2005. [38] G. Qin, J. Wu. Action Refinement for Real-Time Concurrent Processes with Urgency. J. Computer Sci. & Technol., 20(4),514 - 525, 2005. [39] X. Sun, J. Wu. Event-Based Operational Semantics and a Consistency Result for Real-Time Processes with Action Refinement. J. Computer Sci. & Technol., 19(6), 828 - 839, 2004. [40] J. Wu. Symmetric Structure in Logic Programming. J. Computer Sci. & Technol., 19(6), 803 - 811, 2004. [41] J. Wu. CWA Extensions to Multi-Valued Logics. J. Applied Non-Classical Logics, 13(2), 133 – 164, 2003. [42] M. Majster-Cederbaum, J. Wu. Towards Action Refinement for True Concurrent Real Time. Acta Informatica, 39(8), 531 - 577, 2003. [43] H. Fecher, M. Majaster-Cederbaum, and J. Wu. Bundle Event Structures: A Revised Cpo Approach. Information Processing Letters, 83, 7 - 12, 2002. [44] J. Wu. CWA Formalizations in Multi-Valued Logics. J. Computer Sci. & Technol., 16(3), 263 - 269, 2001. [45] J. Wu, M. Lu. On Theorem Proving in Annotated Logics. J. Applied Non-Classical Logics, 10(2), 121 - 143, 2000. [46] J. Wu, Z. Liu. Linear Strategy for Boolean Ring Based Theorem Proving. J. Computer Sci. & Technol., 15(3), 271 - 279, 2000. [47] J. Wu, Z. Liu. Well-Behaved Inference Rules for First-Order Theorem Proving. J. Automated Reasoning, 21(3), 381 - 400, 1998. [48] J. Wu, H. Tan, and Y. Li. An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics. J. Applied Non-Classical Logics, 8(4), 353 - 360, 1998. [49] J. Wu. Mechanical Geometry Theorem Proving Based on Groebner Bases. J. Computer Sci. & Technol., 12(1), 10 - 16, 1997. [50] J. Wu. An Algorithm for Decomposing Zero-Dimensional Polynomial Ideals. J. of Math.(PRC), 17(4), 450 - 454, 1997. [51] J. Wu, L. Li. A method for decomposing zero-dimensional algebraic varieties and its applications. Math. Appl., 10(1), 114 - 118, 1997. [52] J. Wu. Quantitative Properties of Green Equivalences for Special Monoids. J. Sys. Sci. & Math. Sci., 9(3), 198 - 204, 1996. [53] J. Wu. On Algebraic Variety Decomposition. J. Sys. Sci. & Math. Sci., 9(2), 120 - 127, 1996. [54] J. Wu, Z. Liu. On Theorem Proving Using Generalized Odd-Superposition II. Sci. China (Ser. E), 39(6), 608 - 619, 1996. [55] J. Wu, H. Tan. A Method for Automated Geometry Theorem Proving. J. Sys. Sci. & Math. Sci., 9(4), 313 - 319, 1996. [56] L. Zhang, L. Li, and J. Wu. On the Descriptive of Special Thue Systems. Discrete Math., 160(1-3), 291 - 297, 1996.

專著/譯著

[1] J. Wu, Y. Wang, G. Qin. Interactive Markov Chains – Design，Verification and Evaluation of Concurrent Systems (in Chinese). Scientific Publications, Peking, 2007. [2] Y. Wang, J. Wu, J. Jiang. Process Algebra: Symmetry and Action Refinement (in Chinese). Scientific Publications, Peking, 2007.

軟件著作權(quán)

[1] IC驗(yàn)證平臺(tái)“巨微”系統(tǒng)V1.0. 軟件著作權(quán), 登記號(hào): 2006SR06259. [2]“巨微”集成電路等價(jià)驗(yàn)證系統(tǒng)V1.0. 軟件著作權(quán), 登記號(hào): 2007SR00744. [3]“巨微”集成電路形式驗(yàn)證引擎BDD軟件V1.0. 軟件著作權(quán), 登記號(hào): 2007SR18598. [4]“巨微”集成電路形式驗(yàn)證引擎SAT Solver軟件V1.0. 軟件著作權(quán), 登記號(hào): 2007SR20184. [5] 基于交互式馬爾科夫鏈的模型檢測(cè)性能驗(yàn)證平臺(tái)軟件. 軟件著作權(quán), 登記號(hào): 2009SR024924. [6] 代數(shù)符號(hào)計(jì)算模型檢測(cè)軟件. 軟件著作權(quán), 登記號(hào): 2009SR024925. [7] RGPS需求元模型正確性驗(yàn)證工具軟件V1.0. 軟件著作權(quán), 登記號(hào): 2012SR039965. [8] R20關(guān)系數(shù)據(jù)庫(kù)到本體知識(shí)庫(kù)轉(zhuǎn)換工具軟件V1.0. 軟件著作權(quán), 登記號(hào): 2012SR040025. [9] 數(shù)字電路模型檢測(cè)工具軟件V1.0. 軟件著作權(quán), 登記號(hào): 2012SR039989.

獲獎(jiǎng)與榮譽(yù)

德國(guó)“馬普基金”獲得者，中國(guó)科學(xué)院“百人計(jì)劃(國(guó)外引入杰出人才)”入選者，國(guó)家首批“新世紀(jì)百千萬(wàn)人才工程國(guó)家級(jí)人選”，中組部中央直接聯(lián)系高級(jí)專家，國(guó)務(wù)院政府特殊津貼，四川省學(xué)術(shù)和技術(shù)帶頭人，廣西優(yōu)秀專家。

社會(huì)兼職

蘭州大學(xué)信息科學(xué)與工程學(xué)院萃英講席教授;中國(guó)數(shù)學(xué)會(huì)計(jì)算機(jī)代數(shù)專業(yè)委員會(huì)委員;廣西計(jì)算機(jī)學(xué)會(huì)副理事長(zhǎng);四川省專家評(píng)議委員會(huì)委員;廣西科學(xué)技術(shù)獎(jiǎng)勵(lì)委員會(huì)委員;廣西政協(xié)理論研究會(huì)常務(wù)理事。