队伍建设
百人计划
杰出青年
人才招聘
科技副职
二、目前主要研究方向及简介
Myresearchinterestsincludeformalmethodsandsoftwarereliability(logic,formallanguages,theoremproving,modelchecking,correctnessverification)fordevelopinghighqualitysoftware.
Formalmethodsaremathematicallybasedlanguages,techniquesandtoolsforspecifyingandverifyingsoftwaresystems.Formalsoftwaredevelopmentprocessincludesformalspecificationandformalverification.Formalspecificationistheprocessofdescribingthesoftwaresystemusingaformalspecificationlanguage.Formalverificationistheprocessofcarryingoutformalproofsusingformalverificationtechniquesandtools.Useofthiskindofmethodscangreatlyincreasetheunderstandingofasystembyrevealinginconsistencies,ambiguitiesandincompletenessthatmightotherwisegoundetected.Ithasbeenadvocatedasameansofincreasingthereliabilityofsystems,especiallythosewhicharesafetycritical.
三、学习经历
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年获财政部中科院引进国外杰出人才资助
七、代表论著
Cuteliminationandautomaticproofprocedures.
TheoreticalComputerScience91(2):265-284,1991.
Cutformulasinpropositionallogic.
TheoreticalComputerScience120(1):157-168,1993.
Depthofproofs,depthofcut-formulasandcomplexityofcutformulas.
TheoreticalComputerScience129(1):193-206,1994.
VerificationofXYZ/SEprograms.
ChineseJournalofAdvancedSoftwareResearch2(4):364-373,1995.
Numberofmodelsandsatisfiabilityofsetsofclauses.
TheoreticalComputerScience.155(1):277-288,1996.
Analysistreesasamechanicalproofmethod.
ChineseJournalofAdvancedSoftwareResearch4(2):171-179,1997.
Modelcheckingoperatorprocedures.
LectureNotesinComputerScience1680:200-215.Springer-Verlag.1999.
Validationofcontrolsystemspecificationswithabstractplantmodels.
LectureNotesinComputerScience1943:53-62.Springer-Verlag.2000.
ApplyingSDLspecificationsandtoolstotheverificationofprocedures.
LectureNotesinComputerScience2078:421-437.Springer-Verlag.2001.
AStrategyforImprovingtheEfficiencyofProcedureVerification.
LectureNotesinComputerScience2434:113-126.Springer-Verlag.2002.
CombiningStaticAnalysisandCase-BasedSearchSpacePartitioningforReducingPeakMemoryinModelChecking.
JournalofComputerScienceandTechnology18(6):762-770,2003.
八、承担项目
