法國國家信息學與自動化研究院Paris-Rocquencourt研究中心Xavier Rival研究員到軟件所交流
文章來源: | 發布時間:2013-11-19 | 【打印】 【關閉】
11月18日,法國國家信息學與自動化研究院(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研究員作報告
報告會現場