Due to the earthquake and subsequent incidents, we have decided to cancel the following GRACE seminars in March.
Thank you for your understanding.
The 49th GRACE Seminar on Advanced Software Science and Engineering
http://grace-center.jp/
Time: 15:00-16:00, March 16th, 2011
Place:Meeting Room (2009/2010), 20F, National Institute of Informatics
(map)
Inquiry: Soichiro Hidaka (hidaka_AT_nii.ac.jp)
Fee: Free
Please register via the following page:
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.
