北京交通大學計算機與信息技術學院研究生導師：吳盡昭

• 2025考研復試伴學班
• 2025考研復試標準班
• 2026考研英語全程班
• 26考研全科上岸規劃營「擇校▪規劃▪備考」
• 北京交通大學2025考研專業課復習資料「真題▪筆記▪講義▪題庫」

基本信息

姓名：吳盡昭

電子郵件：himrwujzh@aliyun.com

教育背景

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.06-2007.10 中科院成都計算機應用研究所,研究員、博士生導師 2007.10-2009.09 北京交通大學計算機學院,教授、博士生導師 2009.10- 廣西民族大學,教授、副校長

科研項目

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

教學工作

進程代數;模型檢測;計算機科學中的邏輯;人工智能。

論文/期刊

書籍章節 [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.

軟件著作權

[1] IC驗證平臺“巨微”系統V1.0. 軟件著作權, 登記號: 2006SR06259. [2]“巨微”集成電路等價驗證系統V1.0. 軟件著作權, 登記號: 2007SR00744. [3]“巨微”集成電路形式驗證引擎BDD軟件V1.0. 軟件著作權, 登記號: 2007SR18598. [4]“巨微”集成電路形式驗證引擎SAT Solver軟件V1.0. 軟件著作權, 登記號: 2007SR20184. [5] 基于交互式馬爾科夫鏈的模型檢測性能驗證平臺軟件. 軟件著作權, 登記號: 2009SR024924. [6] 代數符號計算模型檢測軟件. 軟件著作權, 登記號: 2009SR024925. [7] RGPS需求元模型正確性驗證工具軟件V1.0. 軟件著作權, 登記號: 2012SR039965. [8] R20關系數據庫到本體知識庫轉換工具軟件V1.0. 軟件著作權, 登記號: 2012SR040025. [9] 數字電路模型檢測工具軟件V1.0. 軟件著作權, 登記號: 2012SR039989.

獲獎與榮譽

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

社會兼職

蘭州大學信息科學與工程學院萃英講席教授;中國數學會計算機代數專業委員會委員;廣西計算機學會副理事長;四川省專家評議委員會委員;廣西科學技術獎勵委員會委員;廣西政協理論研究會常務理事。