2001．5—2004．7， 德国曼海姆大学数学和计算机科学学院， 助理教授；
1996．7—1997．8， 中山市国家税务局， 国家公务员

主持/参与过的项目：
1993.9—1995.8 国防科工委的项目“程序自动生成和验证技术研”。
1993.9—1995.8 “863” 项目“程序设计理论和人工智能研究”。
1994.10—1995.8 江苏省科委的项目“类型理论研究”。
1995.7—1996.7 南京大学，Motorola 公司和Illilois 大学合作的项目“MagicFrame”。
1998.7—2000.5 欧盟KIT 项目“DeTfoRS”。
1997.8—2001.5 国家自然基金委的项目“时序逻辑基础研究”。
2001.5—2004.6 德国国家自然基金委（DFG）的项目“反演系统中的动作精化”。

主要学术成果及获奖经历：
1． 在博士生期间，在导师周巢尘院士的指导下，建立了高阶时段演算理论。该理论提供了研究实时程序设计语言的理论基础。我们为高阶时段演算建立了一个证明系统，并证明在假设所有程序变量是有穷可变的条件下，该证明系统在抽象域上是完备的。我们也运用该理论来处理实时程序设计中的问题，例如，局部变量的声明，局部通道的声明，超稠密计算等。同时，高阶时段演算理论也统一了一些时段演算的变体，例如，经典的时段演算理论，扩充的时段演算理论和所有处理超稠密计算理论等。
2． 运用时段演算理论形式化了调度理论，特别是，我们发现了Liu和Layland的经典Rate Monotonic调度算法中的错误。
3． 提出了一种将层次实现和层次说明相关联的方法，从而可以部分解决了验证大型反演系统中面临的组合爆炸问题。例如，我们的方法支持“予验证”，也就是说，假设抽象实现满足抽象说明，然后用一个低级过程精化某一个抽象动作，并且该过程满足某个性质，那么，根据我们的结论， 可以由这个抽象实现和该过程构造一个低级实现，由这个抽象说明和那个性质构造一个低级说明，并且该低级实现满足这个低级说明。反之，我们也可以将一个复杂的验证问题分解成几个小的验证问题，从而可以克服验证中的空间爆炸问题。
4． 建立了进程代数和模态和时序逻辑的对应关系，从而将进程代数的组合性和时序逻辑的抽象性结合起来。这样，我们就可以对大型反演系统进行组合规范说明，组合实现，当然也可以进行组合验证。为此，我们证明了在模态逻辑中，例如模态µ-演算，类似于进程代数中的“+”是可定义的。利用这种对应关系，我们给出一种组合方法构造上下文无关的进程代数(context-free process algebra) 的特征函数。
读书期间，因学习成绩优秀和科研成绩突出，获得过各类奖学金多项。

1. Dong Shuzhen, Xu Qiwen and Zhan Naijun. “A formal proof of the rate monotonic scheduler”. In the proc. of the Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), part of the federated 1999 International Computer Congress, Hong Kong, December 13-15, 1999. IEEE Computer Society Press.
2. Zhou Chaochen, Dimitar P. Guelev and Zhan Naijun. “A higher-order duration calculus”. In the proc. of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, 13-15 September, 1999.
3. Zhan Naijun. “An intuitive proof for DDS”. Journal of Computer Science and Technology, Vol 15, No.2, 1999.
4. Zhan Naijun. “A higher-order duration calculus and its completeness”. Science in China, Vol 30(5). {中英文版}.
5. Zhan Naijun. “Completeness of higher-order duration calculus”. Presented at and published in the proc. of CSL2000 held in Fischbachau, German, Lecture Notes in Computer Science Vol 1863, Springer-Verlag.
6. Zhan Naijun. “Another formal proof for deadline driven scheduler”. Presented and published in the proc. of RTCSA00 held in Cheju Island, South Korea. IEEE Computer Society Press.
7. Huandong Ma, Liang Li, Jianzhong Wang, Naijun Zhan. “Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol”. Presented at and published in the APSEC'01,
held in Macau. IEEE Computer Society Press.
8. M. Majster-Cederbaum, Naijun Zhan and Harald Fecher. “Action refinement from a logical point of view”. In VMCAI 2003 - Fourth International Conference on Verification, Model Checking and Abstract Interpretation, L.D. Zuck, P.C. Attie, A. Cortesi and S. Mukhopadhyay (Eds.), Lecture Notes in Computer Science 2575, pp.253-267.
9. Naijun Zhan. “Combining hierarchical specification with hierarchical implementation”. Presented at and published in ASIAN'03. Lecture Notes in Computer Science 2896, pp. 110-124. Mumbai, India.
10. Naijun Zhan. “Compsitional properties of sequential processes”. Presented at and Published in SVV'03. Electronic Notes in Theoretical Computer Science. Mumbai,