Sites Inria

English version

Séminaire des équipes de recherche

A Verified Implementation of the Bounded List Container

© INRIA Sophie Auvin - G comme Grille

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.

  • Date : 26/03/2018
  • Lieu : Inria de Paris - 2 rue Simone Iff 75012- Batiment C - Salle Jacques Louis Lions
  • Intervenant(s) : Raphaël Cauderlier

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.

Mots-clés : Séminaire Gallium Equipe de recherche Inria de Paris

Haut de page

Suivez Inria