蛟龙app

当前位置: 首页 >> 师资队伍 >> 博士生导师 >> 正文



吴尽昭

2014年12月23日 14:29  点击:[]

一、基 本 信 息

姓 名

吴尽昭

性 别

出生年月


籍 贯

吉林扶余

专 业

计算机科学与技术

政治面貌

中共党员


学 位

理学博士

外 语

英语、德语


毕业时间及学校

1994年,中国科学院系统科学研究所


专业技术职务

教授、博士生导师

任职时间

2001、2002


工作单位

广西民族大学

职 务

副校长


通信地址

广西南宁市大学东路188号

电 邮

himrwujzh@aliyun.com


教育经历

1984.09-1988.07兰州大学数学系,理学学士

1988.09-1991.07兰州大学计算机科学系,理学硕士(导师:李廉教授)

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- 广西民族大学,教授、副校长、广西混杂计算与集成电路设计分析

重点实验室主任,其间2011年6月至2012年1月挂任大连理工大学校长助理,

自2012年9月起兼任东盟学院院长


学术及社会兼职

中科院成都计算所、北京交通大学兼职教授、博士生导师

兰州大学信息科学与工程学院萃英讲席教授

中国数学会计算机代数专业委员会委员

教育部高校教学指导委员会计算机科学与技术分委会委员

广西计算机学会副理事长

国家自然科学奖励评审专家,国家863项目评审专家

教育部留学回国人员科研启动基金评审专家,科技部国际合作项目评审专家

四川省专家评议委员会委员,广西科学技术奖励委员会委员

广西政协理论研究会常务理事


二、专业领域及专长


(1) 符号计算与自动推理

(1.1) 交换代数与几何定理机器证明

(1.2) Wu-Ritt方法及Groebner基理论

(1.3) 定理自动证明的代数化理论与方法

(1.4) 非经典逻辑架构下的自动推理

(2) 逻辑程序与推理数据库

(2.1)逻辑程序及推理数据库中的代数结构与操作语义

(2.2)基于非经典逻辑的程序设计方法学

(3) 复杂并发系统形式化设计与验证

(3.1)并发系统的刻画语言与形式语义

(3.2)并发系统的组合层次化理论与方法

(3.3)基于定理证明及模型检测的功能验证与性能评估方法与技术

(3.4)微分半代数混杂系统的分析与验证


三、主要学术成绩


系统地建立了自动推理、逻辑程序设计和并发系统设计与分析的代数符号化理论,在普适性、协调性和可计算性三方面取得了实质性突破,开辟了自动推理、逻辑程序设计和复杂并发系统设计与分析的新途径以及代数符号计算新的应用领域。

(1)高效能符号计算与自动推理算法

(1.1)基于布尔多项式余式计算的定理自动证明方法

(1.2)非经典逻辑框架下自动推理的代数化

(1.3)代数簇分解算法的优化策略及其在几何定理机器证明中的应用

(1.4)半群非线性命题的多项式时间判定算法

(2)逻辑程序及推理数据库计算语义

(2.1)对称约简与逻辑程序和推理数据库的计算语义拓广

(2.2)多项式结构应用于非经典逻辑程序的程序设计方法论

(3)高效能高可信复杂并发系统形式化设计与验证分析

(3.1)动作细化及功能行为与性能指标混合并发系统的组合层次化理论

(3.2)包含非协调信息的复杂并发系统的超协调刻画逻辑体系及模型检测技术

(3.3)基于符号计算的并发系统的刻画与验证评估技术

(3.4)微分半代数混杂系统的近似等价理论

(3.5)组合层次化技术在集成电路设计与验证分析中的应用


四、学术奖励与荣誉


(1)德国“马普基金”(1997年)

(2)中国科学院“百人计划(国外引入杰出人才)”入选者(2000年)

(3)国家“新世纪百千万人才工程”国家级人选(2004年)

(4)四川省学术和技术带头人(2005年)

(5)国务院政府特殊津贴(2006年)

(6)中央直接联系高级专家(2006年)

(7)广西壮族自治区优秀专家(2010年)


五、 教学与人才培养


(1) (1)教学

北京大学本科生课程:离散数学、自动推理

德国Mannheim大学本科生课程:计算机科学中的逻辑,可计算性理论,程序语言设计

研究生课程:进程代数,计算机代数,并发系统设计与验证,有限域,代数符号计算

论文奖励:“拓宽基础,强化实践,程序设计语言类课程教学的探索与实践”,全国计算

机教育优秀论文,二等奖,教育部高等学校计算机科学与技术教学指导委员会,2009年

(2) 人才培养

中科院成都计算机应用研究所,指导毕业博士生14名,硕士生16名,目前指导在读博士生

7人,博士后2人,硕士生5人

北京交通大学计算机与信息技术学院,目前指导在读博士6人

兰州大学信息科学与工程学院,指导毕业博士生2人,硕士生13人


六、 主要科研项目


(1) 具有数量指标约束的并发系统的动作细化理论(中科院“百人计划”, 2001-2004年,200万元,主持)

(2) 混合性能模拟的层次化:理论与应用(国家自然科学基金,2004-2006年,23万元,主持)

(3) 混合并发模型的动作细化(德国DFG,2002-2004年,15万欧元,联合主持)

(4) 定理机器证明与自动推理平台(973,2003-2004年,10万元,子课题承担人)

(5) 偏序时序逻辑及其模型检测(德国DFG,2004-2005年,15万欧元,联合主持)

(6) 软件开发与形式化方法(四川省国际合作项目,2004-2005年,10万元,主持)

(7) 集成电路形式验证技术及其软件平台“巨微”系统的研发(科技部中小企业创新基金,2005-2006年,50万元,主持)

(8) 集成电路形式验证平台开发(中科院西部之光联合学者,2005-2006年,30万元,

主研,博士生主持)

(9) 吴方法算法芯片的研发以及基于吴方法的形式化验证技术(973,2005-2009年,

20万元,子课题承担人)

(10)IC形式验证技术及其平台开发(成都市重大科技项目,2005-2006年,70万元,主持)

(11)IC验证技术与平台(四川省科技攻关项目,2006-2007年,20万元,主持)

(12)需求验证与管理(973,2007-2010年,32万元,子课题承担人)

(13)基于代数符号计算的新型软件形式化验证技术和支持工具(863,2007-2009年,

77万元,主持)

(14)复杂并发系统验证和评估分析的代数符号化理论与方法(国家自然科学基金,2009-2011年,35万元,主持)

(15)微分半代数程序模型的等价及等价谱系(国家自然科学基金,2010-2012年,32万元,主持)

(16)嵌入式软件验证与评估若干关键问题研究(教育部博士点基金博导类,2010-2011年,6万元,主持)

(17)现代城市与城际轨道交通运营形式化控制与分析关键技术(广西主席基金项目,2011-2012年,20万元,主持)

(18)大规模集成电路高层次设计验证技术(广西教育厅资助项目,300万元,2011-2013年,主持)

(19)嵌入式软件协同验证与评估(广西自然科学基金,2011-2013年,5万元,主持)

(20)片上多核处理器高层次架构设计的验证理论与关键技术(广西自然科学基金创新研究团队项目,2012-2014年,200万元,主持)

(21)广西混杂计算与集成电路设计分析重点实验室建设项目(广西科技厅,2011年至今,

320万元,主持)

(22)广西“八桂学者”专项(广西自治区人民政府,2011-2015年,800万元,主研)

(23)广西“八桂学者”创新平台(广西教育厅,2012-2015年,70万元,主研)

(24)东盟多语种信息处理研究基地建设(广西教育厅,2012-2014年,50万元,主持)

(25)广西船联网技术研究基地建设(广西教育厅校地校企共建科技创新平台,

2013-2016年,100万元,主持)

(26)近似形式化方法—实微分多项式进程代数研究(国家自然科学基金,2014-2017年,

62万元,主持)


七、科研团队及平台建设情况


(1)广西混杂计算与集成电路设计分析重点实验室(2010年)

(2)中科学院成都计算所博士后流动站广西民族大学基地(2010年)

(3)广西混杂计算与集成电路设计分析 “八桂学者”岗位(2011年)

(4)广西自然科学基金创新研究团队(2012年)

(5)广西船联网技术协同创新中心(2013年)

(6)广西形式化方法“八桂学者”岗位(2013年)


八、国际学术会议


(1)ISIC 2007专题主席 (2)ICSC 2008程序委员会委员

(3)ISCC 2008专题主席 (4)IEEE TrustCom 2008程序委员会委员

(5)IEEE TrustCom 2009程序委员会委员 (6)IEEE TrustCom 2010程序委员会委员

(7)IEEE ICACTE 2010技术委员会主席 (8)IEEE ICCCI 2010大会主席

(9)CRC 2011组委 (10)ISA2012大会主席

(11)ICIC 2013大会主席 (12)MACIS 2013大会主席


九、科研论著及知识产权

专著

[1] J. Wu, Y. Wang, G. Qin.Interactive Markov ChainsDesign,Verification and Evaluationof 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] 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], Jinzhao Wu, , .Derivation of OWL Ontology from XML Documents by Formal Semantic Modeling. 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.

期刊论文(中文)

[57] H. Deng, J. Wu. Approximate Bisimulation Equivalence of Linear semi-Algebraic Transition System(in Chinese).J. Jilin Univ.(Engineering Ed.), 43(4), 1052-1058, 2013.

[58] N. Zhou, J. Wu, Chao Wang.An Invariant Generation Algorithm Based on Wu’s Method(in Chinese).J. Beijing Jiaotong Univ., 36(2), 1-7, 2012.

[59] H. Deng, J. Wu. Bisimulation Equivalence for Polynomial Program Models(in Chinese).J. Beijing Jiaotong Univ., 35(5), 73-77, 2011.

[60] Z. Xu, J. Wu, J. Chen.Design and Implementation of IMC-Based Performance Checker.(in Chinese).J. Computer Applications, 30 (.z1 ): 215-217, 2010.

[61] J. Yang, J. Wu, J. Zhou.Semantic Analysis and Modelling of OWL-S Based on CSP (in Chinese).J.Computer Applications,30 (8): 2173-2176, 2010.

[62] J. Zhou, J. Wu, J. Yang.A Model of Semantic Web Service Process Based on SPIN Checker(in Chinese).J. Computer Applications,30(z1), 2010.

[63] Y. Tang, J. Wu, J. Chen.The Design and Implementation of a SVG-Based Specific Formula Editing Tool (in Chinese). J.Computer Applications, 29(10), 2865 - 2868, 2009.

[64] Z. Liao, J. Wu, H. Tan.Model Checking Technology and Tool Development Based on Groebner Bases (in Chinese).J.Computer Applications, 29(10), 2841 - 2843, 2009.

[65] X. Xu, J. Wu, L. Lin.Model Checking Based on Interactive Markov Chains (in Chinese).J.Computer Applications, 28(07), 1868 - 1871, 2008.

[66] L. Lin, J. Wu. Evolution of Z Specifications with Defaults: A Practical Approach (in Chinese).Computer Science, to appear, 2008.

[67]X. Gao, J. Wu, R. Qiao, W. Yan. A Synchronous Checking Approach to the Optimazation of Non-Classical Slicing (in Chinese).Computer Engineering, to appear, 2008.

[68] R. Qiao, J. Wu. Probabilistic Kleene Algebra with Test (in Chinese).J. Sichuan Univ., to appear, 2008.

[69] L. Zhao, J. Wu. Applying Wu’s Method to Multi-Valued Model Checking (in Chinese).J. Sys. Sci. and Math. Sci., 8, 1020–1029, 2008.

[70] W. Yan, J. Wu, X. Gao.Specifying Multi-Enablings Using Flow Event Structures Based Partial Order Logic (in Chinese).J. Sichuan Univ.(Engineering Sci. Edition), 40(1), 127–132, 2008.

[71] W. Yan, X. Gao, J. Wu. SAT Algorithms Based on Symbolic Simulation and Variable Partitions(in Chinese).J. Sichuan Univ.(Engineering Sci. Edition), 40(3), 121–125, 2008.

[72] Y. Wang, J. Wu, S. Yang.Information Systems Integration Based on Shared Fundamental Data. J.Computer Applications, S1, 2008.

[73] X. Gao, J. Wu, W. Yan, N. Zhou. Overview for Non-Classical Slicing Technique and Its Applications on Formal Verification (in Chinese).Computer Engineering and Applications, 43(36), 43–47, 2007.

[74] Z. Liu, J. Wu. Verification Techniques for Integrated Circuits (in Chinese).China Basic Science, 3, 2007.

[75] F. Qi, J. Wu, D. Xu, W. Yan. Research of Logic Error Diagnosis of Combinnational Circuits (in Chinese).Application Research of Computers,1, 114–116, 2008.

[76] W. Yan, J. Wu, X. Gao.Symbolic Simulation (in Chinese).Computer Engineering, 33(20),27–29,33, 2007.

[77] W. Zhang, J. Wu, Z. Zeng.A Fast JPEG Image Retrieval Approach (in Chinese).Computer Engineering, 31(5), 148 - 149+184, 2005.

[78] J. Wu, H. Yuan. A Simple Operational Semantics Modeling Semantic Action Refinement for Processes with Interrupt (in Chinese).J. of the Graduate School of the Chinese Academy of Sciences, 21(4), 501 - 511, 2004.

[79] W. Zhang, X. Sun, Z. Zeng, J. Wu.Automatic Generation of Mathematical Expressions of Chinese Characters (in Chinese),J. of Computer Research and Development, 41(5), 848 - 852, 2004.

[80] W. Mao, X. Sun, D. Chen, J. Wu.Design of a No Reference Counting Field BDD Package (in Chinese).Journal of Computer Applications, 16(10), 35 - 37, 2004.

[81] J. Wu, Z. Liu. Linear Strategy, Semantic Strategy and Lock Strategy in Remainder Method (in Chinese).Chinese J. Computer, 20(2), 174 - 178, 1997.

[82] H. Tan, J. Wu. Mechanical Demonstration for a Class of Elementary Geometric Theorems (in Chinese).J. Lanzhou Univ., Nat. Sci. 33(3), 31–36, 1997.

[83] J. Wu. Mechanical Theorem Proving in Many-Valued Logics (in Chinese).Chinese J. Computer, 19(10), 773 - 779, 1996.

[84] J. Wu, Z. Liu. On Theorem Proving Using Generalized Odd-Superposition II (in Chinese).Sci. China (Ser. E), 26(5), 442 - 449, 1996.

[85] J. Wu, Z. Liu. Remainder Method for the Mechanical Theorem Proving in First-Order Predicate Calculus (in Chinese).Chinese J. Computer, 19(10), 728 - 734, 1996.

[86] J. Wu, H. Tan. Two Properties of Special Monoids (in Chinese).Acta Mathematica Sinica, 39(5), 643 - 648, 1996.

[87]J. Wu. A Zero-Dimensional Method for Geometry Theorem Proving (in Chinese).J. of Mathematical Research and Exposition, 15(4), 617 - 622, 1995.

国际学术会议论文

[1] Anping He, Daoshe Lu, Jinzhao Wu. A SMT Solver Based on Anthropomorphic and Quasi- Physical.ICACC13, 2013.

[2] Zhiwei Zhang, Jinzhao Wu, Hao Yang. Approximation to Linear Algebraic Transition System.Eighth International Conference on Emerging Intelligent Computing Technology and Applications,Vol.304, 336–343, 2012.

[3] Shaohai Liu, Jinzhao Wu. An algorithm Based on the Local Module Degree for Community Detection in Complex Networks.2012 International Conference on Computer Science and Automation Engineering, 5(1), 232-236, 2012.

[4] Bai Liu,Jinzhao Wu. Polynomial Process Algebra.The 10th World Congress on Intelligent Control and Automation,7, 3004-3007, 2012.

[5] Y. Liu, J. Wu. Dynamic Evolution of Requirement Goal Deployed on Network Environment.Proc. Of the 2012 2ndInternational Conference on Computer and Information Application,IEEE Computer Society Press, Volume 1: 149-152, 2012.

[6] Tingzhao Zhang, Jinzhao Wu. The Consider of RSA Algorithm.3rd International Conference on Information, Electronic and Computer Science, 600-603, 2011.

[7] Yang Liu, Jinzhao Wu. A Formal Method for Finite Relation Model Based on Symbolic Logic.2011 International Conference on Computer Science and Service System(CSSS), IEEE Computer Society Press, Volume 4: 2863-2866,2011.

[8] Yang Liu, Jinzhao Wu. Formal Verification of RGPS-G.2011 International Conference on Computer Science and Service System(CSSS), IEEE Computer Society Press,Volume 4: 3248-3251,2011.

[9] Shaohai Liu, Jinzhao Wu. Rough Sets Based on Concept Lattice Method of Filling the System Risk Assessment.2011 International Conference on Electronics and Optoelectronics (ICEOE), IEEE Computer Society Press, Volume 2: 2119-2122,2011.

[10] Hao Yang, Jinzhao Wu. Formal Verification of RGPS-S.2011 International Conference on Business Computing and Global Information, IEEE Computer Society Press, 599-602, 2011.

[11] Xiangsheng Lu, Jinzhao Wu, Hao yang, Zhiwei Zhang, Xiao Gao. Correctness Verification of RGPS Process Meta-Model.2011 International Conference on Computer and Network Engineering(ICCNE), IEEE Computer Society Press, Volume 2: 195-199, 2011.

[12] Ning Zhou, Jinzhao Wu, Chao Wang, Xinyan Gao. Generating Invariants for Polynomial Transition System.2011 International Conference on Energy Systems and Electrical Power (ESEP), IEEE Computer Society Press, 2011.

[13] Hui Deng, Jinzhao Wu. On Approximate Bisimulation for Polynomial Algebraic Transition Systems.2011 International Conference on Energy Systems and Electrical Power(ESEP), IEEE Computer Society Press, 2011.

[14] Guang Zheng, Jinzhao Wu, Xiaojun He and Aiping Lu. Weaker Bisimulation: How to make a.0+b.0 andτ.a.0+b.0 Equivalent?ICCCI10, V1:440-445, IEEE Computer Society Press, 2010.

[15] Hui Deng, Jinzhao Wu. On Approximate Bisimulation for Polynomial Algebraic Transition Systems.ICCCI10, V2:585-589, IEEE Computer Society Press, 2010.

[16] Ning Zhou, Jinzhao Wu and Cao Wang. Generating Non-Linear Invariant for Polynomial Transition System.ICCCI10, V2:590-594, IEEE Computer Society Press, 2010.

[17] Weidong Tang, Sen Niu, Jinzhao Wu and Yang Liu.Security Analysis on Internet of Things.ICCCI10, V4:235-237, IEEE Computer Society Press, 2010.

[18] Xinmei Yang, Jinzhao Wu.Symbolic Simulation via SAT Solver with Variable Parition.ICCCI10, V4:522-526, IEEE Computer Society Press, 2010.

[19] Yang Liu, Jinzhao Wu, Jin Zhou and Hao Yang. Decomposition Model Building and Ontology Reasoning Towards G-Layer of RGPS Requirement Meta-Model.ICACTE10Session 2, 47-51, IEEE Computer Society Press, 2010.

[20] Jianfeng Chen and Jinzhao Wu. GMC: A Performance Model Checker for Concurrent Systems.ICACTE10Session 1, 6-10, IEEE Computer Society Press, 2010.

[21] Jianshu Yang, Jinzhao Wu, and Jiajia Fang. A Semantic Model for OWL-S Based on Timed CSP.

ICACTE10Session 6, 250-254, IEEE Computer Society Press, 2010.

[22] Zhenxing Xu and Jinzhao Wu. Ontology Reasoning and Services Composition Verification towards O-RGPS Requirement Meta-Model.ICACTE10Session 7, 273-277, IEEE Computer Society Press, 2010.

[23] Lin Zhao, Tao Tang, Jinzhao Wu, and Tianhua Xu. Runtime Verification with Multi-Valued Formula Rewriting.4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 77-86,IEEE Computer Society Press, 2010.

[24] Jianfeng Chen, Jinzhao Wu. Performance Evaluation by Ant Colony Algorithm,ITCS10,IEEE Computer Society Press, 2010.

[25] S. Yang, J. Wu. Mapping Relational Databases into Ontologies through a Graph-Based Formal Model.6th Int. Conf. On Semantics, Knowledge and Grids, 219–226,IEEE Computer Society Press, 2010.

[26] J. Wu, S. Yang. Process Algebra Approach to Verifying Safety Specification of Hybrid Embedded Systems.ICCSN09, 129–133,IEEE Computer Society Press, 2009.

[27] H. Hou, J. Wu. Quasi-Classical Description Logics and Paraconsistent Reasoning in the Semantic Web.ASWC08 Workshop Proc., AIT e-Press, 54–69, 2008.(ISBN:978-947-8257-64-8)

[28] L. Lin, J. Wu. Open Logic Based on Partial-Ordered Partition Model.TASE'08, 247 - 254, IEEE Computer Society Press, 2008.

[29] X. Gao, J. Wu, R. Qiao, J. Chen. Theory Framework for Event Structure Slicing.ISCC08, 714 - 721, IEEE Computer Society Press, 2008.

[30] R. Qiao, J. Wu, Y. Wang, X. Gao.Operational Semantics of Probabilistic Kleene Algebra with Test.ISCC08, 706 - 713, IEEE Computer Society Press, 2008.

[31] R. Qiao, J. Wu, X. Gao.Probabilistic Modal Kleene Algebra and Hoare-Style Logic.ICNC08, 652 - 661, IEEE Computer Society Press, 2008.

[32] J. Wu, S. Yang. Timed CSP for Safety Specification of Hybrid Systems.TrustCom08, 1913 - 1918, IEEE Computer Society Press, 2008.

[33] A. He, J. Wu, L. Li. The Causality based Denotational Semantics for SystemC.Proceedings of Circuit and System, IASTED, 2008.

[34] A. He, J. Wu, L. Li. An Eficient Algorithm for Transforming LTL Formula to Buchi Automaton.Proc. Of ICICTA08, 1215-1220, 2008.

[35] G. Zheng, J. Wu, L. Li.Stochastic Process Algebra with Value-Passing.CSSE08,IEEE Computer Society Press, 2008.

[36] J. Wu, W. Yan. A Logic for Flow Event Structures.22ndInternational Conference on Computers and Their Applications(CATA’07), 373 - 379, 2007.

[37] J. Wu, W. Yan. Model Checking of Computer based Systems.14thAnnual IEEE International Conference and Workshop on the Engineering of Computer Based Systems(ECBC’07), 557–568, IEEE Computer Society Press, 2007.

[38] J. Wu,L. Zhao. An Algebraic Approach to Multi-Valued Model Checking.ACSD'07, 238 - 239, IEEE Computer Society Press, 2007.

[39] J. Wu, L. Zhao. Multi-Valued Model Checking via Groebner Basis Approach.1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering(TASE'07), 35–44, IEEE Computer Society Press, 2007.

[40] D. Chen, J. Wu. QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems.1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), 241–250, IEEE Computer Society Press, 2007.

[41] J. Jiang, J. Wu, H. Shu.Symmetry in Process Algebra.TASE'07, 450–462, IEEE Computer Society Press, 2007.

[42] G. Zheng, S. Li, J. Wu, L. Li.A Non-Interleaving Denotational Semantics of Value-Passing

CCS with Action Refinement. FAW’07,Lecture Notes in Computer Science, 4613, 178–190, 2007.

[43] J. Jiang, J. Wu, L. Xu.An Architecture for Software Systems.ACIS-SNPD07,154–159, IEEE Computer Society Press, 2007.

[44] J. Wu, W. Yan. Model Checking Action-Based Event Structure Logic for Finite-State Concurrent Programs,AWCVS06, 2006.

[45] D. Chen, J. Wu. Reasoning about Inconsistent Concurrent Systems: A Non-Classical Temporal Logic. SOFSEM'06,Lecture Notes in Computer Science, 3831, 207 - 217, 2006.

[46] J. Jiang, J. Wu. Symmetry in Event Structures.ACM SAC'06 Track on Software Verification, 1850–1851, ACM Press, 2006.

[47] X. Chao, L. Li, J. Wu. Simulation for Interactive Markovian Chains. ICNC-FSKD’06,Lecture Notes in Computer Science, 4221, 893–902, 2006.

[48] D. Chen, J. Wu. Model Checking Temporal Aspects of Inconsistent Concurrent Systems Based on Paraconsistent Logic.SVV'05,ENTCS, 157(1), 23–38, 2005.

[49] J. Jiang, J. Wu. Symmetry and Autobisimulation.PDCAT'05, 866–870, IEEE Computer Society Press, 2005.

[50] J. Jiang, J. Wu, and W. Yan. Structural Reductions in Process Algebra Languages.JICC'05, 596 - 600, World Scientific Publications, 2005.

[51] N. Zhan, J. Wu. Compositionality of Fixpoint Logic with Chop.ICTAC'05,Lecture Notes in Computer Science, 3722, 136 - 150, 2005.

[52] J. Jiang, J. Wu.The Preservation of Interleaving Equivalences.ICECCS'05, IEEE Computer Society Press, 580 - 589, 2005.

[53] W. Zhang, J. Wu, X. Sun, J. Tang. JPEG Image Retrieval Based on Salient Points.The IEE International Conference on Visual Information Engineering(VIE 2005), 2005.

[54] J. Wu, W. Zhang, Z. Zeng.Automatic Generation of Mathematical Expression of a Chinese Character.4thIASTED International Conference on Computational Intelligence(CI'05), 404 - 408, ACTA Press, 2005.

[55] W. Zhang, X. Sun, J. Wu.An Approach to Compressed Image Retrieval Based on JPEG2000 Framework. ADMA'05,LNAI, 2005.

[56] X. Sun, J. Wu. Operational Semantics for Real-Time Processes with Action Refinement.SEFM'05, IEEE Computer Society Press, 54 - 63, 2005.

[57] W. Mao, J. Wu. Application of Wu's Method to Symbolic Model Checking.ISSAC'05, 237 - 244, ACM Press, 2005.

[58] M. Majster-Cederbaum, J. Wu, H. Yue,& N. Zhan.Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. ICFEM'04,Lecture Notes in Computer Science, 3308, 449 - 463, 2004.

[59] X. Sun, J. Wu, X. Song, M. Majster-Cederbaum.Formal Specification of an Asynchronous Processor via Action Refinement.MTV'04, IEEE Computer Society Press, 142 - 148, 2004.

[60] J. Wu, H. Yue. Action Refinement for Concurrent Systems with Causal Ambiguity.SEFM'04, IEEE Computer Society Press, 300 - 309, 2004.

[61] G. Qin, J. Wu. Branching time Equivalences for Interactive Markov Chains. EPEW'04,Lecture Notes in Computer Science, 3236, 156 - 169, 2004.

[62] G. Qin, J. Wu. Action Refinement for Real-Time Processes with Urgency. ARTS'04,ENTCS, 139(1), 123 - 144, 2004.

[63] M. Majster-Cederbaum, J. Wu.Adding Action Refinement to Stochastic True Concurrency Models.

ICFEM'03,Lecture Notes in Computer Science, 2885, 226 - 245, 2003.

[64] J. Wu. Symmetry and Logic Programming.Proc. 32 JAIIO - WAIT'03, Argentinian Workshop on Theoretical Computer Science, 2003.

[65] H. Fecher, M. Majster-Cederbaum, J. Wu.Action Refinement for Probabilistic Processes

with True Concurrency Models. PAPA-Probmiv'02,Lecture Notes in Computer Science, 2399, 77 - 94, 2002.

[66] H. Fecher, M. Majster-Cederbaum, J. Wu.Action Refinement in a Real-Time Process Algebra with a True Concurrency Models. REFINE'02,Electronic Notes in Theoretical Computer Science, 70(3), 2002.

[67] M. Majster-Cederbaum, J. Wu.Action Refinement for True Concurrent Real-Time.ICECCS'01, IEEE Computer Society Press, 58 - 68, 2001.

[68] J. Wu. Action Refinement in Timed LOTOS. ASCM'01,Lecture Notes on Computing, 9, 183 - 192, World Scientific Publ., 2001.

[69] J. Wu. Logic Programming -- Taking Advantage of Symmetry. ASCM'00,Lecture Notes on Computing, 8, 100 - 109, World Scientific Publ., 2000.

[70] J. Wu. Symmetry and Logic Programming.Proc. 11th Nordic Workshop on Programming Theory, Department of Information Technology, Uppsala University, Sweden, 1999.

[71] J. Wu, M. Lu. Extending CWA into Multi-Valued Logics.ASCM'98, Lanzhou Univ. Press, China, 259 - 271, 1998.

[72] J. Wu, Z. Liu. On First-Order Theorem Proving.ASCM'96, Scientists Incorporated, Japan, 163 - 168, 1996.

[73] J. Wu, Z. Liu. Remainder Method for the First-Order Theorem Proving.ASCM'95, Scientists Incorporated, Japan, 91–98, 1995.

[74] J. Wu, H. Tan. An Algebraic Method to Decide the Deduction Problem in Propositional Many-Valued Logics.ISMVL'94, IEEE Computer Society Press, 1994.

[75] J. Wu, L. Li. Green Equivalences and Regular Problem for Special Monoids.ISSAC'93, ACM Press, New York, 78 - 85, 1993.

 

研究报告

[1] Wu, J., Symmetries in Logic Programs,Research Report MPI-I-1999-2-005, Max-Planck-Institut fur Informatik, Germany, 1999.

[2] Wu, J., Ma, B., On the Theorem Proving using First-Order Polynomials,Research Report No.30, Institute of Mathematics & School of Mathematical Sciences, Peking University, 1996.

[3] Wu, J., The Decomposition of Algebraic Differential Varieties,Research Report No.29, Institute of Mathematics & School of Mathematical Sciences, Peking University, 1996.

[4] Wu, J., Mechanical Geometry Theorem Proving via Groebner Bases,Research Report No.25, Institute of Mathematics & School of Mathematical Sciences, Peking University, 1996.

[5] Wu, J., Inferences Rules Compatible with Set-Of-Support Strategy and Linear Strategy,Research Report No.24, Institute of Mathematics & School of Mathematical Sciences, Peking Uni, 1996.

[6] Wu, J., First-Order Polynomial Based Theorem Proving,Research Report No.23, Institute of Mathematics & School of Mathematical Sciences, Peking Uni, 1996.

[7] Wu, J., Liu, Z., On the Proof System using Odd-Superposition II, in:MM-Res. Preprints, 14, Institute of Systems Science, Academia Sinica, 1996.

[8] Wu, J., Liu, Z., The Remainder Method for Mechanical Theorem Proving in First-Order Predicate Calculus (Extended Abstract), in:MM-Res. Preprints, 13, Institute of Systems Science, Academia Sinica, 1995.

[9] Wu, J., Du, H., An Algorithm for Decomposing Zero-Dimensional Polynomial Ideals, in:MM-Res. Preprints, 12, Institute of Systems Science, Academia Sinica, 1994.

[10] Du, H., Wu, J., Irreducible Sequences of Varieties and Applications, in:MM-Res. Preprints, 12, Institute of Systems Science, Academia Sinica, 1994.

[11] Li, L., Wu, J., A Method for Decomposing Zero-Dimensional Algebraic Varieties and its Applications, in:MM-Res.Preprints, 11, Institute of Systems Science, Academia Sinica,1994.

[12] Wu, J., The Decomposition of Algebraic Varieties -- Algorithm and Applications, in:MM-Res. Preprints, 10, Institute of Systems Science, Academia Sinica, 1993.

[13] Du, H., Wu, J., On the Computation of Zero-Dimensional Ideals, in: MM-Res. Preprints, 10, Institute of Systems Science, Academia Sinica, 1993.

[14] Wu, J., A Special Case of Wu's Method, in:MM-Res. Preprints,9, Institute of Systems Science, Academia Sinica, 1993.

[15] Wu, J., The Primary Decomposition of Polynomial Ideals, in:MM-Res. Preprints, 8, Institute of Systems Science, Academia Sinica, 1992.

[16] Wu, J., Li, L., The Decidability of Regular Problem for Special Monoids, in:MM - Res. Preprints, 7, Institute of Systems Science, Academia Sinica, 1992.

专利

[1]吴尽昭,杨世翰,陈剑峰.企业多遗留系统的基础数据交换验证平台.申请号:200810045874.3

[2]吴尽昭,陈剑峰,杨世翰.企业应用集成平台构建方法和体系结构.申请号:200810045875.8

[3]陈剑峰,吴尽昭,杨世翰.基于交互式马尔可夫链模型检测的嵌入式系统性能评价技术方案.

申请号:200910059677.1

软件著作权

[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.

十、近三年工作计划

(一)科研

并发系统(软件/硬件/协议)复杂程度的剧增,使得功能行为与性能指标变得密不可分,同时,传统形式方法通常不包含数据的交换与处理,无助于实际工程应用。总体目标是通过符号、数值计算与并发理论的交叉、融合与应用研究,构建功能行为、性能指标和数据结构三维统一的并发混杂系统的验证与评估理论。




 

 

 

 

 

 

 


 

功能性为、性能指标和数据处理,涵盖了并发系统设计与分析的所有核心要素,拟建立的理论统一了含有这些要素的系统刻画模型以及功能验证和性能评估方法,避免了功能与性能局部分析所造成的重复甚至矛盾,具有全局普适性,同时,数据结构的引入导致近似计算成为可能,可以满足实际工程需求。由于混杂计算方法的计算操作丰富,带误差但误差可控,计算能力强大,使得验证与评估方法的计算方式和计算能力得到丰富和强化。由于各自领域的局限性,目前国际上还少有通过混杂计算的手段和途径进行复杂并发系统设计与分析的系统和完整的研究工作。

理论研究方面,目前的工作主要集中在以下几个方面:(1)混杂系统的近似等价及其谱系;(2)混杂系统的组合层次化理论与技术;(3)近似模型检测技术;(4)非经典逻辑框架下的混杂系统理论;(5)混杂系统理论与方法与测试模拟技术的有效结合与实现。

实际应用方面,目前主要开展混杂系统理论与方法在(1)网络式软件系统设计与分析中的应用;(2)大规模集成电路验证与评估软件平台系统设计与开发中的应用;(3)轨道交通列车运行控制与安全系统设计中的应用。

(二) 研究生培养

每年招收、指导和培养符号计算、自动推理与复杂并发系统形式化设计与分析交叉理论

与方法研究方向的博士学位研究生2至3名,硕士学位研究生3至4名。

(三) 教学

承担数学和计算机理论基础方面的课程,如离散数学、数理逻辑、抽象代数、计算机代数、算法分析与设计、数据结构、人工智能、自动推理、进程代数、形式化方法等。

 










附:指导毕业及在读博士研究生和博士后情况

(1)毕业博士研究生

岳厚光(中科院成都计算所,2003年9月-2006年7月,博士学位论文:并发系统动作精化的研究及其在UML中的应用,毕业后在上海交通大学从事博士后研究)

孙秀莉(中科院成都计算所,2003年9月-2006年7月,博士学位论文:基于动作细化的异步电路自动综合,毕业后在美国Portland州立大学从事博士后研究,现在美国Intel California工作)

张问银(中科院成都计算所2003年9月-2006年7月,博士学位论文:汉字数学表达式的自动生成,毕业后在华东师范大学工作)

覃广平(中科院成都计算所,2004年9月-2007年7月,博士学位论文:交互式马尔科夫链--理论与应用,毕业后在上海拓普科技有限公司工作)

闫 炜(中科院成都计算所,2004年9月-2007年7月,博士学位论文:事件结构的对称约简及其逻辑系统,毕业后在电子科技大学工作)

蒋建民(中科院成都计算所,2004年9月-2007年7月,博士学位论文:对称与动作细化,毕业后在福建师范大学工作)

陈冬火(中科院成都计算所,2004年9月-2007年7月,博士学位论文:超协调时序逻辑及其模型检测方法,毕业后在南京大学从事博士后研究,现在苏州大学工作)

林连南(中科院成都计算所,2004年9月-2007年7月,博士学位论文:需求演化理论--基于偏序划分模型的开放逻辑,毕业后在华南理工大学工作)

乔 瑞(中科院成都计算所,2005年9月-2008年7月,博士学位论文:概率克林代数,毕业后在武汉理工大学工作)

高新岩(中科院成都计算所,2005年9月-2009年7月,博士学位论文:面向高层描述的字级符号模拟技术研究,毕业后在大连理工大学工作)

陈剑峰(中科院成都计算所,2005年9月-2009年7月,博士学位论文:基于交互式马尔可夫链的模型检验,毕业后在电子30所工作)

杨世瀚(中科院成都计算所,2006年9月-2009年7月,博士学位论文:动态模型检测的不变性理论研究,毕业后在中科院成都分院、广西民族大学工作)

赵 林(中科院成都计算所,2006年9月-2009年7月,博士学位论文:基于代数符号计算的多值模型检验,毕业后在北京交通大学轨道交通控制与安全国家重点实验室工作)

郑 光(兰州大学,2007年9月-2010年7月,博士学位论文:并发系统的动作细化理论,毕业后在中国中医科学院从事博士后研究)

何安平(兰州大学,2008年9月-2011年7月,博士学位论文:基于层次模型的混合系统形式化分析与验证,毕业后在中科院成都计算所从事博士后研究,在广西民族大学工作)

刘 洋(中科院成都计算所,2009年9月-2013年7月,博士学位论文:网络式软件需求模型的形式化验证方法研究,毕业后在重庆邮电大学工作)

(2)在读博士研究生

周 宁(北京交通大学,2009年9月-,博士学位论文题目:微分半代数程序模型的近似迹等价)

付 军(北京交通大学,2009年9月-,博士学位论文题目:微分半代数逻辑的近似推理理论)

邓 辉(北京交通大学,2009年9月-,博士学位论文题目:微分半代数程序模型的近似互模拟等价)

赵 榕(中科院成都计算所,,2009年9月-,博士学位论文题目:网络式软件异层等价性验证)

王 超(北京交通大学,2010年9月-,博士学位论文题目:微分半代数事件结构的近似等价)

杨 浩(中科院成都计算所,2010年9月-,博士学位论文题目:线性代数混杂系统的等价及等价谱系)

刘绍海(中科院成都计算所,,2010年9月-,博士学位论文题目:网络自动推理技术)

刘 白(中科院成都计算所,2010年9月-,博士学位论文题目:代数变迁系统的动作细化理论)

汤卫东(中科院成都计算所,2010年9月-,博士学位论文题目:代数事件结构的动作细化理论)

阎 硕(北京交通大学,2011年9月-,博士学位论文题目:基于混杂系统模型的轨道交通控制系统)

张志伟(中科院成都计算所,,2011年9月-,博士学位论文题目:代数混杂系统近似完备迹等价)

黄留佳(北京交通大学,2012年9月-,博士学位论文题目:片上多核处理器高层次架构设计的

模型检测技术)

钟淑瑛(中科院成都计算所,2012年9月-,博士学位论文题目:片上多核处理器高层次架构设计

的等价理论)

汤 琳(中科院成都计算所,2012年9月-,博士学位论文题目:片上多核处理器设计核配置问题研究)

谢 盈(中科院成都计算所,2013年9月-,博士学位论文题目:实微分多项式进程代数)

张 晖(中科院成都计算所,2013年9月-,博士学位论文题目:近似形式化方法)

(3)在站博士后

黄 勇(中科院成都计算所,2010年9月-,研究方向:嵌入式系统的形式化验证技术)

何安平(中科院成都计算所,2011年9月-,研究方向:异步电路设计验证)

 

 

 

 

 

 

 

 

上一条:王东明 下一条:刘振海

关闭



蛟龙app  地址:广西南宁市大学东路188号
电话:3260133  邮编:530006