【主要学术经历】

1986年9月-1987年12月 英国爱丁堡大学计算机科学基础实验室 Research Fellow
1988年1月-1990年3月 中国科学院软件研究所 副研究员
1990年4月-1993年4月 英国Sussex大学 Research Fellow
1993年 中国科学院软件研究所 研究员
1994年 中国科学院软件研究所 博士生导师
1999年 中国科学院软件所计算机科学开放研究实验室 主任
1990年 《软件学报》 编委
1994年 中国计算机学会理论计算机科学专业委员会 副理事长
1997年 中国科技大学研究生院 兼职教授
1999年 《计算机学报》中、英文版 编委

【代表论著】

1. H. Lin, PAM: A Process Algebra Manipulator. Formal Methods in System Design, Vol.7, No.3, pp. 243-259. 1995. Kluwer Academic Publishers.
2. H. Lin, A Verification Tool for Value-Passing Process Algebras. IFIP Transactions C-16: Protocol Specification, Testing and Verification, pp. 79-92. 1993. North-Holland.
3. M. Hennessy and H. Lin, Symbolic Bisimulations. Theoretical Computer Science, Vol. 138, pp. 353-389. 1995. Elsevier.
4. M. Hennessy and H. Lin, Proof Systems for Message-Passing Process Algebras. Formal Aspects of Computing. Vol.8, pp397-407. 1996. Springer-Verlag.
5. H. Lin, Symbolic Transition Graph with Assignment,Proc. 7th Int. Conf. on Concurrency Theory, Pisa, Italy, August 26-29, 1996. Lecture Notes in Computer Science Vol. 1119, pp. 50-56. Springer-Verlag.
6. H. Lin, "On-the-fly Instantiation" of Value-passing Processes. Proc. Joint International Conferences on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification, Paris, France, November 1998. pp. 215-230. Kluwer Academic Publishers.
7. H. Lin, Complete Inference Systems for Weak Bisimulation Equivalences in the pi-Calculus. Proc. 6th International Joint Conference on Theory and Practice of Software Development, Aarhus, Denmark, May 1995. Lecture Notes in Computer Science, Vol. 915, pp. 187-201. Springer-Verlag.
8. H. Lin, Unique Fixpoint Induction for Mobile Processes. Proc. 6th International Conference on Concurrency Theory. Philadelphia, U.S.A., August 1995. Lecture Notes in Computer Science, Vol. 962, pp. 88-102. Springer-Verlag.
9. H. Lin, Complete Proof Systems for Observation Congruences in Finite Control pi-Calculus. Proc. of 25th International Colloquium on Automata, Languages and Programming, Aalborg, Denmark, July 1998. Lecture Notes in Computer Science Vol. 1443, pp. 443-454. Springer-Verlag.
10. H. Lin, Procedural Implementation of Algebraic Specifications. ACM Transactions on Programming Languages and Systems, Vol.15, No.5, pp. 876-895. 1993. ACM Press.

【重要贡献】

　　林惠民研究员长期从事计算机程序，特别是并发程序的形式语义学及形式化方法的研究。他在进程代数的验证工具、消息传送进程的语义理论和π-演算的公理化等方向上取得了突破性进展，其主要贡献包括：

1. 设计并实现了世界上第一个通用的进程代数验证工具

　　进程代数的实际应用离不开计算机辅助工具的支持。八十年代后期，一批进程代数验证工具应运而生（如CWB, PSF, LOTOSphere等），其共同局限性是每一工具只适用于某一特定的进程演算。这种局限性妨碍了验证工具的推广应用。如何克服这种局限性是当时国际进程代数界面临的一个重大挑战。 　　这些验证工具无法做到通用，根本原因在于缺乏既能描述不同进程演算的语义，又能为计算机所理解的通用语言。经过对不同演算的反复比较，并考虑到在计算机上实现的可能性，林提炼出了一个元语言，用它可以描述各种进程演算的公理化语义，并且具有良好的可读性。在此基础上实现了通用的交互式进程代数验证工具PAM[1]，只要将这个元语言描述的进程演算定义输入PAM，就得到该演算的证明器。PAM可同时接受多个不同的演算，对每个演算又可生成多个证明窗口。这是世界上第一个通用的进程代数证明工具。 　　1993年林又利用当时刚刚取得的关于消息传送进程证明系统的理论结果，对PAM加以扩充，研制成迄今世界上唯一能对付消息传送进程的验证工具VPAM[2]。

　　PAM和VPAM都是通过ftp在Internet上公开发行的，其用户遍布各大洲，包括美国、加拿大、英、法、德、意、荷兰、丹麦、瑞典、斯洛伐克、巴西、印度、新西兰、南非等十几个国家，其中既有来自大学的，也有来自菲利普、惠普和贝尔等著名公司实验室的。

　　PAM对进程代数验证工具的发展产生了深刻的影响。1996年美国ACM“并发研究中的战略方向”报告中两次引用了这一工作（详见附件“引用情况摘录”）。

2. 与Hennessy教授合作提出、并独立发展了“符号互模拟”理论，在消息传送进程研究中取得突破性进展。

　　并发理论研究的核心问题是进程间的通讯（消息传送）。可是在传统进程代数的理论研究中，为了数学处理的方便，通讯被简化为单纯的同步。从消息传送进程到单纯同步演算的过渡由一转换完成，其核心步骤是把输入动作翻译成遍历数据域的选择算子。当数据域无穷时,这是个无穷算子,而在实际问题中数据域往往是无穷的。这种无穷算子的引入使得进程代数的很多理论结果无法付诸应用，耗费大量人力物力开发研制的验证工具也难以用于解决实际问题。

　　林惠民与英国Sussex大学的Hennessy 教授合作，提出了“符号互模拟理论”[3]，其基本出发点是不依赖上述转换而直接建立消息传送进程的语义理论。这一理论将输入视为一种抽象的动作，而不是将其实例化，从而避免了因数据域无穷而带来的无穷性。这里要克服的主要困难是在执行抽象输入动作后，进程项可能含有自由变量，即成为开项，而传统进程代数理论所使用的语义模型只能解释不含自由变量的闭项。为此[3]中引入了“符号迁移图”作为开项的语义模型，在此基础上建立了符号互模拟理论。在[4]中又进一步建立了消息传送进程互模拟的相对完备证明系统。

　　“符号迁移图”解决了传统转换方法带来的无穷分枝问题，但有穷符号迁移图在并行复合下不封闭(即两个有穷符号迁移图并行复合的结果可能是无穷深度的符号迁移图)。林在第七届国际并发理论会议上提出了“带赋值的符号迁移图”[5]，被国际同行称为“不受限制的带参正则进程的恰当的模型”（见附件“引用情况摘录”），圆满地解决了这个问题。在98年11月巴黎举行的第六届分布式系统及通讯协议的形式描述技术与第十八届协议规约、测试与验证联合国际会议上，林进一步发表了基于有穷带赋值符号迁移图的互模拟判定算法[6]。

　　符号互模拟理论突破了进程代数中将消息传送进程转换为（带无穷算子的）“基本”进程的传统做法，为在计算机上对消息传送进程进行推理和验证奠定了理论基础。这一理论被国际同行称为“Hennessy和林理论”，不仅被应用于消息传送进程的研究，而且也应用到对π-演算、模态逻辑、以及实时进程的研究中，推动了这些研究领域的发展（详见附件“引用情况摘录”）。

3. 彻底解决了π-演算的有穷公理化问题

　　为了描述移动式通讯,ACM图林奖获得者Milner教授与其合作者于1989年正式提出π-演算（也称“移动进程演算”）。π-演算研究中的一个基本问题是刻划进程的互模拟等价关系。π-演算的最初文献中只给出常（ground）强互模拟的公理系统。四年以后,π-演算的提出者之一发表了一般强互模拟的完备公理系统，但没能解决更为困难的弱互模拟的公理化问题。这一问题成为π-演算研究中一个激烈竞争的热点。

　　林针对π-演算建立了符号互模拟的理论，在95年5月第六届国际软件开发的理论与实践会议上发表了π-演算迟、早两种弱互模拟的完备证明系统[7]。在同年8月美国费城举行的第六届国际并发理论会议上国际同行引用这一成果时指出：“时至今日,π-演算的迟弱互模拟的公理化只在[Lin95]中借助于符号互模拟的概念得到。”（见附件 “引用情况摘录”）

　　为了对π-演算中递归定义的无穷进程进行推理，在第六届国际并发理论会议上林在π-演算中引入“进程抽象”的构造，提出了适用于π-演算的唯一不动点归纳法[8]，并进一步于98年7月在第三十五届ICALP大会上发表了有穷控制π-演算弱互模拟的完备证明系统[9]。这一结果彻底解决了π-演算的有穷公理化问题，使我国在这一竞争极为激烈的研究方向上处于国际领先地位。

　　据目前收集到的资料，1991年以来有54篇国外公开发表的文献引用了林惠民的研究工作（不含自引用），其中20篇收录在SCI中。这些引用文献有的详细报道了如何应用PAM解决实际问题及所得到的结果，有的将PAM与类似工具进行比较，指出PAM优于其它工具之处。在对符号互模拟工作的引用中，有的说明他们的理论是依照Hennessy和林的理论和方法建立的，有的指出他们的结果是在Hennessy和林工作的基础上取得的，有的指出他们的工作是受Hennessy和林工作的启发。在对林关于π-演算工作的引用中，有的指出林的结果先于他们的相应结果，有的认为遵循林的思想可以将他们已有的结果进一步推广。具体引用情况请参见附件“引用情况摘录”。

　　1996年7月在日本举行的“并发理论与应用”国际研讨会邀请林惠民作关于π-演算证明系统的特邀报告。1999年1月美国NASA的科学与工程计算机研究所邀请林专程赴美作关于形式化方法的讲座。最近他又受到邀请将在第八届国际数值分析与计算机科学及应用讨论会（1999年8月）上作特邀报告。由此可见林的工作在国际上所受到的重视。

　　此外，近年来提供费用邀请林去作专题学术讲座的还有包括法国INRIA、巴黎高师、英国爱丁堡大学、美国宾州大学等十余所欧、美高等学府和科研机构。