| |
|
|
| 一、基本信息 |
| 姓名： |
张文辉 |
| 职务： |
|
| 职称： |
研究员 |
| 性别： |
男 |
| 联系电话： |
|
| 电子邮件： |
zwh(at)ios.ac.cn |
所在部门： |
计算机科学国家重点实验室 |
| 通讯地址： |
北京中关村南四街4号（北京8718信箱）中国科学院软件研究所 |
| 邮政编码： |
100190 |
| 个人主页： |
http://lcs.ios.ac.cn/~zwh/ |
|
|
| 二、目前主要研究方向及简介 |
My research interests include formal methods and software reliability (logic, formal languages, theorem proving, model checking, correctness verification) for developing high quality software.
Formal methods are mathematically based languages, techniques and tools for specifying and verifying software systems. Formal software development process includes formal specification and formal verification. Formal specification is the process of describing the software system using a formal specification language. Formal verification is the process of carrying out formal proofs using formal verification techniques and tools. Use of this kind of methods can greatly increase the understanding of a system by revealing inconsistencies, ambiguities and incompleteness that might otherwise go undetected. It has been advocated as a means of increasing the reliability of systems, especially those which are safety critical. |
| 三、学习经历 |
1976-1978福建宁德地区民族中学
1978-1979北京大学
1979-1988挪威奥斯陆大学 |
| 四、工作经历 |
1986-1986挪威INENCO公司
1987-1987挪威奥斯陆大学
1988-1989中科院软件所
1989-1989香港Citibank公司
1989-1991挪威奥斯陆大学
1991-1993挪威Telemark学院
1993-1994中科院软件所
1994-1995挪威Telemark学院
1995-1997挪威Achilles公司
1997-2001挪威能源技术研究所
2001-2004中科院软件所 |
| 五、社会兼职 |
|
| 六、研究成果与获奖情况 |
主要从事形式化方法及相关领域的研究，在程序的形式验证、逻辑推理、模型检测、软件系统设计方法的形式化等方面有一定的研究积累。在自动推理的研究方面，对谓词公式中的量词和其它逻辑联结词作了详细的分析。区分了引理中它们的使用对证明的复杂性的不同影响。在这基础上分析了连接法和消解法及其变种与可自由使用引理的逻辑系统的关系，论证了这些方法在引理使用上的不同的局限性，加深了对自动定理证明方法的不足的认识，并揭示了扩展的消解法，即允许表示定义的重言子句集合加到初始子句集合进行消解，其功能实质上就是为了增加复杂引理应用的可能性，以提高推理效率。在这些工作的基础上，提出了一个分析模型个数的算法和一个命题逻辑公式判定的算法，取得了良好的理论效果。这方面的工作对认识自动定理证明的困难本质和命题逻辑公式判定算法的研究起到了一定的推动作用。在模型检测的研究方面，将模型检测方法应用于操作程序的验证，提出了多种针对具体应用做抽象和分不同情况以降低模型检测空间和时间复杂性的方法，包括将操作程序和操作环境的模型用中间进程分开，递增式地对操作环境进行建模和逐级验证以降低模型检测的应用门槛；基于对应用目标和模型的分析，将应用领域的特殊性质嵌入到模型及性质描述中以降低模型检测的复杂性；结合对模型的静态分析，将所选的不同情况嵌入到性质描述中以降低模型检测的复杂性。这方面的工作对模型检测在不同领域的应用有一定的借鉴作用。
1993年获王宽诚科研奖金资助
2002年获财政部中科院引进国外杰出人才资助 |
| 七、代表论著 |
Cut elimination and automatic proof procedures.
Theoretical Computer Science 91(2):265-284, 1991.
Cut formulas in propositional logic.
Theoretical Computer Science 120(1):157-168, 1993.
Depth of proofs, depth of cut-formulas and complexity of cut formulas.
Theoretical Computer Science 129(1):193-206, 1994.
Verification of XYZ/SE programs.
Chinese Journal of Advanced Software Research 2(4):364-373, 1995.
Number of models and satisfiability of sets of clauses.
Theoretical Computer Science. 155(1):277-288, 1996.
Analysis trees as a mechanical proof method.
Chinese Journal of Advanced Software Research 4(2):171-179, 1997.
Model checking operator procedures.
Lecture Notes in Computer Science 1680:200-215. Springer-Verlag. 1999.
Validation of control system specifications with abstract plant models.
Lecture Notes in Computer Science 1943:53-62. Springer-Verlag. 2000.
Applying SDL specifications and tools to the verification of procedures.
Lecture Notes in Computer Science 2078:421-437. Springer-Verlag. 2001.
A Strategy for Improving the Efficiency of Procedure Verification.
Lecture Notes in Computer Science 2434:113-126. Springer-Verlag. 2002.
Combining Static Analysis and Case-Based Search Space Partitioning for Reducing Peak Memory in Model Checking.
Journal of Computer Science and Technology 18(6):762-770, 2003.
|
|
|
