IRILL - Research and Innovation on Free Software When: April 11th, 15h45
Where: Irill, 3rd floor
Abstract : Claire Dross (Adacore)
Title: Use formal methods to verify an Ada program with SPARK2014
Abstract:
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.