队伍建设
百人计划
杰出青年
人才招聘
科技副职
二、目前主要研究方向及简介
实时和混成系统、并发计算模型、程序验证
三、学习经历
1997．9—2000．9，中科院软件所和联合国大学国际软件技术研究所，攻读博士学位；
1993．9—1996．7，南京大学计算机系，攻读硕士学位；
1989．9—1993。7，南京大学数学系，读本科
四、工作经历
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的经典RateMonotonic调度算法中的错误。
3．提出了一种将层次实现和层次说明相关联的方法，从而可以部分解决了验证大型反演系统中面临的组合爆炸问题。例如，我们的方法支持“予验证”，也就是说，假设抽象实现满足抽象说明，然后用一个低级过程精化某一个抽象动作，并且该过程满足某个性质，那么，根据我们的结论，可以由这个抽象实现和该过程构造一个低级实现，由这个抽象说明和那个性质构造一个低级说明，并且该低级实现满足这个低级说明。反之，我们也可以将一个复杂的验证问题分解成几个小的验证问题，从而可以克服验证中的空间爆炸问题。
4．建立了进程代数和模态和时序逻辑的对应关系，从而将进程代数的组合性和时序逻辑的抽象性结合起来。这样，我们就可以对大型反演系统进行组合规范说明，组合实现，当然也可以进行组合验证。为此，我们证明了在模态逻辑中，例如模态µ-演算，类似于进程代数中的“+”是可定义的。利用这种对应关系，我们给出一种组合方法构造上下文无关的进程代数(context-freeprocessalgebra)的特征函数。
读书期间，因学习成绩优秀和科研成绩突出，获得过各类奖学金多项。
七、代表论著
1.DongShuzhen,XuQiwenandZhanNaijun.“Aformalproofoftheratemonotonicscheduler”.Intheproc.oftheSixthInternationalConferenceonReal-TimeComputingSystemsandApplications(RTCSA'99),partofthefederated1999InternationalComputerCongress,HongKong,December13-15,1999.IEEEComputerSocietyPress.
2.ZhouChaochen,DimitarP.GuelevandZhanNaijun.“Ahigher-orderdurationcalculus”.Intheproc.oftheSymposiuminCelebrationoftheWorkofC.A.R.Hoare,Oxford,13-15September,1999.
3.ZhanNaijun.“AnintuitiveproofforDDS”.JournalofComputerScienceandTechnology,Vol15,No.2,1999.
4.ZhanNaijun.“Ahigher-orderdurationcalculusanditscompleteness”.ScienceinChina,Vol30(5).{中英文版}.
5.ZhanNaijun.“Completenessofhigher-orderdurationcalculus”.Presentedatandpublishedintheproc.ofCSL2000heldinFischbachau,German,LectureNotesinComputerScienceVol1863,Springer-Verlag.
6.ZhanNaijun.“Anotherformalprooffordeadlinedrivenscheduler”.Presentedandpublishedintheproc.ofRTCSA00heldinChejuIsland,SouthKorea.IEEEComputerSocietyPress.
7.HuandongMa,LiangLi,JianzhongWang,NaijunZhan.“AutomaticSynthesisoftheDCSpecificationsofLipSynchronisationProtocol”.PresentedatandpublishedintheAPSEC'01,
heldinMacau.IEEEComputerSocietyPress.
8.M.Majster-Cederbaum,NaijunZhanandHaraldFecher.“Actionrefinementfromalogicalpointofview”.InVMCAI2003-FourthInternationalConferenceonVerification,ModelCheckingandAbstractInterpretation,L.D.Zuck,P.C.Attie,A.CortesiandS.Mukhopadhyay(Eds.),LectureNotesinComputerScience2575,pp.253-267.
9.NaijunZhan.“Combininghierarchicalspecificationwithhierarchicalimplementation”.PresentedatandpublishedinASIAN'03.LectureNotesinComputerScience2896,pp.110-124.Mumbai,India.
10.NaijunZhan.“Compsitionalpropertiesofsequentialprocesses”.PresentedatandPublishedinSVV'03.ElectronicNotesinTheoreticalComputerScience.Mumbai,
八、承担项目
