Use formal methods to verify an Ada program with SPARK2014
Speaker(s) : Claire DROSS (Adacore)
From the beginning, the Ada language was designed for critical software. It is still mostly used for the development of such systems. To facilitate the expression of requirements for the verification of programs, the last update of the Ada language includes new capabilities, such as contracts on functions or type invariants. With the increase cost of unit testing, the certification standards are opening to formal methods as a new way to address verification activities. Therefore, more and more users are interested in using formal methods for verifying part of their software.
In this talk, we present the upcoming version of the SPARK subset of Ada. It aims at easily allowing formal analysis on parts of an Ada program. We then give some hints on how formal verification is conducted in this tool. Finally, we explain how formal proof can be used in combination with more traditional testing.
Emmanuel.Chailloux (at) nulllip6.fr