Huimin LIN Laboratory for Computer Science Institute of Software Chinese Academy of Sciences P.O.Box 8718 Beijing 100190 P.R.China Fax:   +86 10 62661627

I am a research professor in the Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences. The laboratory is committed to basic as well as application-oriented research in computer science, with focus on fundamental software research. It is still expanding and have several positions, including visiting positions, available. If you are interested in doing research in Beijing, or just coming for a visit, then please contact me or other people in the lab whose areas are close to yours.

Research interests: Concurrency, Process algebras, Value-passing, Mobility, Model checking, Modal logics and mu-Calculus, Tools and algorithms for concurrent systems, Formal methods.

Publications

• H. Lin, A Predicate mu-Calculus for Mobile Ambients. Journal of Computer Science and Technology. Vol.20, No. 1, pp.95-104, 2005. [paper.ps.gz

] Talks given at China-Germany Joint Workshop on Theoretical Computer Science, Shanghai, Oct. 15-17, 2003, and International Workshop on Formal Methods and Security, Nanjing, May 17-20, 2004. [slides.ps]

• H. Lin, Complete Inference Systems for Weak Bisimulation Equivalences in the pi-Calculus. Information and Computation. 180(1), 1-29 (2003). Academic Press. [paper.ps.gz

] An extended abstract of this paper appeared in TAPSOFT'95, Aarhus, Denmark, May 1995. LNCS 915. pp. 187-201.

• H. Lin and Wang Yi, Axiomatising Timed Automata. Acta Informatica. 38, 277-305 (2002). Springer-Verlag. [paper.ps.gz] An extended abstract of this paper appeared in FST&TCS'2000, New Delhi, December 2000. LNCS 1974, pp.277-289.
• M. Hennessy, H. Lin and J. Rathke, Unique Fixpoint Induction for Message-Passing Process Calculi. Science of Computer Programming 41(3), 241-275 (2001). Elsevier.
• H. Lin, Model Checking Value-passing Processes. 8th Asia-Pacific Software Engineering Conference (APSEC'2001), Macau, December 4-7, 2001. [paper.ps.gz]
• A. Ingolfsdottir and H. Lin, A Symbolic Approach to Value-passing Processes. Chapter 7 of Handbook of Processes Algebra. Elsevier. 2001. [paper.ps.gz]
• H. Lin and Wang Yi, A Proof System for Timed Automata. FOSSACS'2000, Berlin, March/April 2000. LNCS 1784, pp.208-222. [paper.ps.gz]
• H. Lin, Computing Bisimulations for Finite-Control pi-Calculus. Journal of Computer Science and Technology, Vol.15, No. 1, 2000. [paper.ps.gz]
• H. Lin, Inference Systems for Observation Equivalences in the pi-Calculus (in Chinese). Science in China (Series E), Vol.29, No.5, pp.452-463. 1999.
• H. Lin, "On-the-fly" Instantiation of Value-passing Processes. FORTE/PSTV'98, Paris, November 1998. pp. 215-230. Kluwer Academic Publishers. [paper.ps.gz]
• H. Lin, Complete Proof Systems for Observation Congruence in Finite-Control pi-Calculus. ICALP'98, Aalborg, Denmark, August 1998, pp. 443-454. LNCS 1443. Springer. [paper.ps.gz]
• M. Hennessy and H. Lin, Unique Fixpoint Induction for Message- passing Process Calculi. CATS'97, Sydney, Australia, Feb. 1997, pp. 122-131. [paper.ps.gz]
• H. Lin, On Removing Unguarded Recursions in The pi-Calculus (in Chinese). Journal of Software. Vol. 8, pp. 321-326. 1997.
• M. Hennessy and H. Lin, Proof Systems for Message-passing Process Algebras. Formal Aspects of Computing, Vol. 8, pp. 379-407. 1996. Springer. [paper.ps.gz]
• H. Lin, Symbolic Transition Graph with Assignment. CONCUR'96, Pisa, Italy, August 1996. pp. 50-65. LNCS 1119. [paper.ps.gz]
• H. Lin, PAM: A Process Algebra Manipulator. Formal Method in Systems Design, Vol. 7, No. 3, pp. 243-259, 1995. Kluwer Academic Publishers. [paper.ps.gz] An extended abstract of this paper appeared in CAV'91, Aalborg, Denmark, July 1991. LNCS 575. pp. 136-146.
• M. Hennessy and H. Lin, Symbolic Bisimulations. Theoretical Computer Science, Vol. 138, pp. 353 - 389, 1995. Elsevier.
• H. Lin, Unique Fixpoint Induction for Mobile Processes. CONCUR'95, Philadelphia, USA, August 1995, pp. 88-102. LNCS 962. [paper.ps.gz]
• H. Lin, On Implementing Unique Fixpoint Induction for Value-passing Processes. TACAS'95, Aarhus, Denmark, May 1995. [paper.ps.gz]
• H. Lin, Proof Systems for the pi-Calculus (in Chinese). Advances in Theoretical Computer Science, Nov 1994. pp. 1-5.
• H. Lin, Symbolic Bisimulations and Proof Systems for the Pi-Calculus. Sussex University Computer Science Report 1994:07. [paper.pdf]
• H. Lin, Procedural Implementation of Algebraic Specifications. ACM Transactions on Programming Languages and Systems, Vol. 15 No. 5, pp. 876-895, 1993. ACM Press.
• H. Lin, A Verification Tool for Value-Passing Processes. 13th IFIP Symposium on Protocol Specification, Testing and Verification, Liege, Belgium, May 1993. pp. 79-92. North-Holland. [paper.ps.gz]
• H. Lin, An Interactive Proof Tool for Process Algebras. 9th Symposium on Theoretical Aspects of Computer Science, Paris, Feb. 1992. LNCS 577.
• H. Lin and M.C. Pong, Modeling Multiple Inheritance with Colimits. Formal Aspects of Computing, Vol. 2 No.4, pp. 301-311, 1990. Springer.