概率程序上断言的形式化分析

Speaker:    符鸿飞教授，上海交通大学
Time:          12月31日 15:00-17:00 
Location:    信息学院 1A 200
Host:           宋富教授
Abstract:
概率程序在一般命令式程序的基础上添加诸如概率分支、概率赋值等概率语句，在针对随机性系统以及随机算法的建模与分析方面具有潜在的应用价值。断言是描述程序正确性性质的一类基本机制，考察程序在某些关键位置上的关键条件是否被满足或不被满足。在概率程序中，断言一般用于描述程序关键位置上的关键条件是否以极高的概率被满足或不被满足。本报告将阐述基于不动点定理的断言形式化分析方法，并基于约束求解给出指数型断言概率紧致上下界的算法。

Bio:
符鸿飞，上海交通大学John Hopcroft计算机科学中心助理教授，博士毕业于德国亚琛工业大学，目前主要研究概率层面的形式化方法理论，成果涵盖概率模型检验以及概率程序验证两个子领域。概率模型检验方面成果涵盖马尔可夫链以及马尔可夫决策过程等基本概率模型上的模型检验理论、计算复杂性以及自动化模型检验算法，其中部分成果发表在欧洲理论计算机科学协会旗舰学术会议ICALP上，并获得信息物理系统形式化方法国际旗舰学术会议HSCC颁发的最佳学生论文奖。概率程序验证方面成果涵盖概率程序终止性、灵敏性、定量分析等各种基础关键性质的验证理论和自动化验证算法，成果发表在形式化方法和程序语言理论国际著名学术会议及期刊CAV、POPL、PLDI、TOPLAS等，其中部分成果经整理发表在由国际著名出版社剑桥大学出版社出版的专著章节中。