姓名：贺飞
出生日期：1980.12
职务：副教授
Email:hefei@tsinghua.edu.cn
地址：清华大学东主楼11-307室，100084

教育背景2002.09－2008.01，清华大学计算机系，获工学博士学位
1998.09－2002.07，国防科技大学计算机学院，获工学学士学位
工作履历2011.12–至今，清华大学软件学院，副教授
？2008.05–2011.12，清华大学软件学院，讲师
学术兼职PCmemberofICECCS2013,co-chairofVTECS2013
讲授课程：
《软件形式化验证》，《嵌入式系统建模与分析技术》

研究领域形式化验证理论及其在嵌入式系统、软件系统中的应用
研究概况NSFC面上项目：基于归纳不变式的模型检测研究，2013.1–2016.12（主持）
NSFC青年项目：基于假设/保证自动推理的组合验证研究,2010.1-2012.12（主持）
NSFC重点项目：基于定理证明的可信嵌入式软件建模与验证平台研究,2008.1-2010.12（参与）
NSFC-ANR中法合作交流项目：嵌入式系统仿真与验证平台开发,2009.1-2011.12(参与)
973项目：产品设计软件系统的部件级可验证性理论研究,2010.1-2015.12（参与）

学术成果SELECTEDJOURNALPUBLICATIONS
1.LiangzeYin,FeiHe,WilliamN.N.Hung,XiaoyuSongandMingGu,MaxtermCoveringforSatisfiability,IEEETransactionsonComputers,61(3),pp.420-426,March,2012.
2.FeiHe,XiaoyuSong,WilliamN.N.Hung,MingGuandJiaguangSun,IntegratingEvolutionaryComputationwithAbstractionRefinementforModelChecking,IEEETransactionsonComputers,vol.59,no.1,pp.116-126,Jan.2010.
3.FeiHe,XiaoyuSong,MingGuandJiaguangSun,Heuristic-GuidedAbstractionRefinement,ComputerJournal,52(3),pp.280-287,May,2009.
4.FeiHe,WilliamN.N.Hung,XiaoyuSong,MingGuandJiaguangSun,ASatisfiabilityFormulationforFPGARoutingwithPinRearrangements,InternationalJournalofElectronics,Vol.94,No.9,pp.857-868,2007.
5.FeiHe,XiaoyuSong,MingGu,GuowuYang,WilliamN.N.HungandJiaguangSun,ProbabilisticOptimizationforBoard-LevelRoutingProblem,IEEETransactionsonCircuitsandSystemsII,Vol.53,No.4,pp.264-268,April,2006.
SELECTEDCONFERENCEPUBLICATIONS
6.HuiKong,FeiHe,XiaoyuSong,WilliamN.N.HungandMingGu,Exponential-Condition-BasedBarrierCertificateGenerationforSafetyVerificationofHybridSystems,acceptedbyCAV2013.
7.WenruiMeng,FeiHe,Bow-YawWang,andQiangLiu,Thread-ModularModelCheckingwithIterativeRefinement,4thInternationalConferenceonNASAFormalMethods(NFM2012),Norfolk,Virginia,USA,April3–5,2012,pp.237-251.
8.MinZhou,FeiHeandMingGu,AnEfficientResolutionBasedAlgorithmforSatisfiabilityProblem.5thIEEEInternationalConferenceonTheoreticalAspectsofSoftwareEngineering(TASE2011),Xi'an,China,August29-31,2011,pp.60--67.
9.Yu-FangChen,EdmundM.Clarke,AzadehFarzan,FeiHe,Ming-HsienTsai,Yih-KuenTsay,Bow-YawWang,andLeiZhu,ComparingLearningAlgorithmsinAutomatedAssume-GuaranteeReasoning,4thInternationalSymposiumonLeveragingApplicationsofFormalMethods,Verification,andValidation(ISoLA2010),Heraklion,Crete,Greece,October18-21,2010,pp.643--657.
10.FeiHe,HeZhu,WilliamN.N.Hung,XiaoyuSongandMingGu,CompositionalAbstractionRefinementforTimedSystems,20104thIEEEInternationalSymposiumonTheoreticalAspectsofSoftwareEngineering,August25-27,2010,pp.168-176.
11.MinZhou,FeiHe,Bow-YawWang,MingGu,OnArrayTheoryofBoundedElements,22ndInternationalConferenceonComputerAidedVerification(CAV2010),Edinburgh,UK,July15-19,pp.570-584,2010.
12.HeZhu,FeiHe,WilliamN.N.Hung,XiaoyuSongandMingGu,DataMiningBasedDecompositionforAssume-GuaranteeReasoning,9thInternationalConferenceonFormalMethodsinComputer-AidedDesign(FMCAD2009),Austin,TX,USA,Nov.15-18,pp.116-119,2009.
13.FeiHe,LucianoBaresi,CarloGhezziandPaolaSpoletini,FormalAnalysisofPublish-SubscribeSystemsbyProbabilisticTimedAutomata,27thIFIPWG6.1InternationalConferenceonFormalMethodsforNetworkedandDistributedSystems(FORTE2007),Tallinn,Estonia,June27-29,pp.247-262,2007.
14.FeiHe,XiaoyuSong,MingGuandJiaguangSun,AProbabilisticLearningApproachforCounterexampleGuidedAbstractionRefinement,Proceedingsofthe4thInternationalSymposiumonAutomatedTechnologyforVerificationandAnalysis(ATVA2006),LNCS4218,Beijing,China,October23-26,pp.39-50,2006.
15.AnduoWang,FeiHe,MingGuandXiaoYuSong,VerifyingJavaProgramsbyTheoremProverHOL,30thAnnualInternationalComputerSoftwareandApplicationsConference(COMPSAC2006),Chicago,US,September17-21,pp.139-142,2006.