3月16日(水)開催予定の第49回GRACEセミナーは、
東北地方太平洋沖地震発生に伴う影響を考慮し、
開催中止とさせて頂きます。
何卒、ご理解のほど、よろしくお願いいたします。
GRACEセンター事務局
主催：NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
http://grace-center.jp/
日時：2011年3月16日（水）15:00-16:00
場所：国立情報学研究所(NII) 20階ミーティングルーム室 (2009/2010)（地図）
参加費：無料
お問い合わせ：日高 宗一郎(hidaka_AT_nii.ac.jp)_AT_を＠に書き換えてください。
参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://grace-center.jp/regist/seminar
==========================================================
Speaker:
Pierre-Loïc Garoche (ONERA, the French Aerospace Lab)
Title:
Analyzing Lustre programs by combining K-induction (based on SMT solvers) and Abstract Interpretation
Abstract:
In this talk, we will present our approach for verifying properties on Lustre-like programs. Lustre is a synchronous language which is widely used to model control systems. As far as we know one of the most efficient method to address verification issues for these programs and ensure their safety is model-checking, based on the k-induction principle and SMT solvers. But one of the major drawback of this approach is the need of external inputs, mainly done by humans nowadays, to reinforce the description of the system to help the analysis to converge. Our proposal is based on a specific collaboration between a k-induction procedure and an abstract interpreter to evaluate safety properties and inject lemmas describing the system during the k-induction process.
This talk will present the Lustre language, the k-induction method tooled with SMT solvers and finally our approach to collaboration between techniques.
This work has been done in collaboration with Pierre Roux and Rémi Delmas, from Onera.
