法国国家信息学与自动化研究院Paris-Rocquencourt研究中心Xavier Rival研究员到软件所交流

文章来源:  |  发布时间:2013-11-19  |  【打印】 【关闭

  

1118日,法国国家信息学与自动化研究院(INRIA) Paris-Rocquencourt研究中心Xavier Rival研究员应计算机科学国家重点实验室的邀请到软件所进行学术交流,并作了题为Modular Construction of Shape-Numeric Analyzers的学术报告。

在报告中,Xavier Rival阐述了他与合作者近期在软件静态分析领域的研究成果。静态分析是通过分析程序源代码而近似地推导出程序运行行为的关键性质,以验证程序的正确性或检测源代码中可能含有的错误。目前静态分析研究所关注的性质大致可分为两类:一类为数据的构形(shape), 如指针、动态内存、递归数据结构等;另一类为数据的数值计算,如浮点数据的计算。如何有效地分析推导出程序中数据在构形与数值计算的整体性质是静态分析的难点之一。Rival与合作者提出了针对这一难点的一个能将各种针对数据构形与针对数据计算的静态分析算法有机集成的基础架构,以及相应的静态分析算法。

报告结束后,与会人员就相关问题与Xavier Rival研究员进行了广泛而深入的讨论。 

XavierRival现任法国国家信息学与自动化研究院Paris-Rocquencourt研究中心研究员,研究方向为基于抽象解析(abstract interpretation)架构的程序静态分析方法。Rival分别于2005年及2011年从巴黎高等师范学院(École Normale Supérieure取得计算机科学博士学位和特许任教(Habilitation)资格。自2001年起一直参与法国国家科学研究中心(CNRS)、巴黎高等师范学院、法国国家信息学与自动化研究院的静态分析联合研究项目(Astrée。该项目于2001年启动,其成果曾应用于空中客车公司A380机型飞行控制代码的自动分析。

Xavier Rival研究员作报告

报告会现场