Title: A Verified Implementation of the Bounded List Container

Speaker: Mihaela Sighireanu, IRIF, University of Paris Diderot (Paris7), France.

Time: 3:00 pm, September 13th (Thursday), 2018.

Venue: Lecture room (334), 3rd Floor, Building 5, Software Park, Chinese Academy of Sciences.

Abstract:

　　I will present a work that contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides constant time methods to update the list by adding, deleting, and changing elements, as well as cursors for list traversal and access to elements. The library is implemented in C, but we wrote the code and its specification by imitating the ones provided by GNAT for the standard library of Ada 2012. The proof of functional correctness is done using VeriFast, which provides an auto-active 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. This case study may be of interest for other verification platforms, thus we highlight the intricate points of its proof.

　　This is a joint work with R. Cauderlier, published at TACAS 2018.

Short biography:

　　Mihaela Sighireanu is associate professor at University of Paris Diderot and member of the IRIF. She did a PHD on the definition of formal modelling language based on timed process algebras at INRIA Rhone-Alpes. She obtained an habilitation on directed research on automated verification (by static analysis or deductive verification) of programs manipulating the heap. She developed several tools for analysing C programs and for solving entailment problems in separation logic.