基本信息 办公电话： 电子邮件： 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.
获奖与荣誉 德国“马普基金”获得者，中国科学院“(国外引入杰出人才)”入选者，国家首批“新世纪百千万人才工程国家级人选”，中组部中央直接联系高级专家，国务院政府特殊津贴，四川省学术和技术带头人，广西优秀专家。
社会兼职 兰州大学信息科学与工程学院萃英讲席教授；中国数学会计算机代数专业委员会委员；广西计算机学会副理事长；四川省专家评议委员会委员；广西科学技术奖励委员会委员；广西政协理论研究会常务理事。