Mário José PARREIRA PEREIRA
Will publicly defend his PhD thesis
Tools and Techniques for the Verification of Modular Stateful Code
supervised by M. Jean-Christophe FILLIÂTRE
Defense on Monday, December the 10th 2018, at 14h00
Place: Laboratoire de Recherche en Informatique Bât 650 Ada Lovelace, Université Paris Sud, 91405 Orsay Cedex France
salle des thèses PCRI
The jury is composed by the following members
M. Jean-Christophe FILLIâTRE | CNRS | Supervisor | ||
M. Jorge SOUSA PINTO | Universidade do Minho | Reviewer | ||
M. Wolfgang AHRENDT | Chalmers University of Technology | Reviewer | ||
Mme Catherine DUBOIS | École Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise | Examiner | ||
Mme Mihaela SIGHIREANU | Université Paris Diderot | Examiner | ||
M. Xavier LEROY | INRIA | Examiner | ||
M. Laurent FRIBOURG | CNRS | Examiner |
Keywords : | Deductive verification, Why3, Effects, OCaml library, Modular |
Abstract : |
This thesis is set in the field of formal
methods, more precisely in the domain of deductive program
verification. Our working context is the Why3 framework, a set of
tools to implement, formally specify, and prove programs using
off-the-shelf theorem provers. Why3 features a programming language,
called WhyML, designed with verification in mind. An important
feature of WhyML is ghost code: portions of the program that are
introduced for the sole purpose of specification and
verification. When it comes to get an executable implementation,
ghost code is removed by an automatic process called extraction. One
of the main contributions of this thesis is the formalization and
implementation of Why3's extraction. The formalization consists in
showing that the extracted program preserves the same operational
behavior as the original source code, based on a type and effect
system. The new extraction mechanism has been successfully used to
get correct-by-construction OCaml modules, which are part of a
verified OCaml library of data structures and algorithms. This
verification effort led to two other contributions of this thesis.
The first is a systematic approach to the verification of
pointer-based data structures using ghost models of fragments of the
heap. A fully automatic verification of a union-find data structure
was achieved using this technique. The second contribution is a
modular way to reason about iteration, independently of the
underlying implementation. Several cursors and higher-order
iterators have been specified and verified with this
approach.
DirectionsFrom Paris, by Le Guichet
From Paris, by Massy-Palaiseau
|