Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 26 mars, 10h30

                              ------------------
                              Raphaël Cauderlier
                              ------------------

                                     IRIF

           =======================================================
           A Verified Implementation of the Bounded List Container
           =======================================================

Standard libraries of programming languages provide efficient
implementations for common data containers. The details of these
implementations are abstracted away by generic interfaces which are
specified in terms of well understood mathematical structures such as
sets, multisets, sequences, and partial functions. The intensive use of
container libraries makes important their formal verification.

I will present a case study of full functional verification of the
bounded doubly-linked list container of from the standard library of Ada
2012. This library is specified in SPARK and several client programs
depend on this specification.

However, the low-level invariants required to verify this library cannot
be expressed in SPARK. For this reason, the proof of functional
correctness is done using VeriFast, a verification environment for
Separation Logic extended with algebraic data types. The specifications
proved entail the contracts of the Ada library and include new
features. The verification method we used employs a precise algebraic
model of the data structure and we show that it facilitates the
verification and captures entirely the library contracts.