代表性著作：
时间：
交互式马尔科夫链-并发系统的设计、验证与评估 科学出版社 2007
进程代数-对称与动作细化 科学出版社 2007
代表性论文：
First-Order Polynomial Based Theorem Proving. Mathematics Mechanization and Applications Academic Press, London, 273 - 294 2000
Green Equivalences and Regular Problem for Special Monoids ISSAC'93, ACM Press, New York, 78 - 85 1993
An Algebraic Method to Decide the Deduction Problem in Propositional Many-Valued Logics ISMVL'94, IEEE Computer Society Press 1994
Remainder Method for the First-Order Theorem Proving ASCM'95, Scientists Incorporated, Japan, 91 – 98 1995
On Theorem Proving Using Generalized Odd-Superposition II Sci. China (Ser. E), 39(6), 608 - 619 1996
Mechanical Geometry Theorem Proving Based on Groebner Bases J. Computer Sci. & Technol., 12(1), 10 - 16 1997
Well-Behaved Inference Rules for First-Order Theorem Proving J. Automated Reasoning, 21(3), 381 - 400 1998
Symmetry and Logic Programming. Proc. 11th Nordic Workshop on Programming Theory Uppsala Uni., Sweden 1999
Linear Strategy for Boolean Ring Based Theorem Proving J. Computer Sci. & Technol., 15(3), 271 - 279 2000
CWA Formalizations in Multi-Valued Logics J. Computer Sci. & Technol., 16(3), 263 - 269 2001
Bundle Event Structures: A Revised Cpo Approach Information Processing Letters, 83, 7 - 12 2002
Towards Action Refinement for True Concurrent Real Time Acta Informatica, 39(8), 531 - 577 2003
Symmetric Structure in Logic Programming J. Computer Sci. & Technol., 19(6), 803 - 811 2004
Action Refinement for Real-Time Concurrent Processes with Urgency J. Computer Sci. & Technol., 20(4),514 - 525 2005
Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity Acta Informatica, 42（6-7）, 389 – 418 2006
Multi-Valued Model Checking via Groebner Basis Approach TASE'07, 35 – 44, IEEE Computer Society Press 2007
Probabilistic Modal Kleene Algebra and Hoare-Style Logic ICNC’08, 652 - 661, IEEE Computer Society Press 2008
Process Algebra Approach to Verifying Safety Specification of Hybrid Systems ICCSN’09, 129 – 133, IEEE Computer Society Press 2009
Ontology Reasoning and Services Composition Verification towards O-RGPS Requirement Meta-Model ICACTE’10, 273-277, IEEE Computer Society Press 2010
专利：
企业多遗留系统的基础数据交换验证平台 申请号：**4.3
企业应用集成平台构建方法和体系结构 申请号：**5.8
基于交互式马尔可夫链模型检测的嵌入式系统性能评价技术方案 申请号：**7.1
知识产权：
IC验证平台“巨微”系统V1.0 软件著作权，登记号: 2006SR06259
“巨微”集成电路等价验证系统V1.0 软件著作权，登记号: 2007SR00744
“巨微”集成电路形式验证引擎BDD软件V1.0 软件著作权，登记号: 2007SR18598.
“巨微”集成电路形式验证引擎SAT Solver软件V1.0 软件著作权，登记号: 2007SR20184
“基于交互式马尔科夫链的模型检测平台软件. 软件著作权，登记号: 2009SR024924
“代数符号计算模型检测软件 软件著作权，登记号: 2009SR024925
近三年科研计划：
通过符号计算与并发系统设计与分析理论的交叉、融合与应用研究，构建功能行为、性能指标和数据结构三维统一的并发系统（软件/协议/硬件）的验证与评估理论、方法和技术。
联系方式：
Email: himrwujz@yahoo.com.cn
如果发现导师信息存在错误或者偏差，欢迎随时与我们联系，以便进行更新完善。联系方式
