Programming-Testing-Proving
- Domaine
- Programming-Testing-Proving
- Domain - extra
- Data intensive systems certification
- Année
- 2012
- Starting
- september/october 2012
- État
- Open
- Sujet
- Toward Data Certification
- Thesis advisor
- BENZAKEN Véronique
- Co-advisors
- CONTEJEAN Evelyne, CR CNRS LRI Proval
- Laboratory
- Collaborations
- Part of the work will be related to the ANR Project TYPEX
- Abstract
- The aim of this thesis is to certify data intensive systems using formal tools such as SMT provers (e.g., Alt-ergo) embedded in the Why3 platform as well as interactive theorem provers (e.g., Coq).
- Context
- Program verification and certification have been intensively studied in the last decades yielding very impressive results and highly reliable software (e.g., the comp cert project). Surprisingly, while the amount of data stored and managed by data engines have drastically increased thus needing for fully reliable systems, little attention have been devoted to certify such systems.
- Objectives
- The aim of this thesis is to equip data intensive systems such as relational database systems, XQuery and semi structured engines with the same kind of tools thus providing fully certified systems.
- Work program
- A first goal of this thesis is to equip data systems with a mean to automatically and statically (at compile time) prove that updates will preserve invariants if such is the case. To do so we shall rely on the Why3 platform. Why3 takes as input a program equipped with its specification, and computes a logical formula the validity of which is equivalent to the fact the input program satisfies the given specification.
A second part of the PhD thesis will consist in adapting the previous approach to different data models with a particular emphasis to XML and JSON semi-structured formats and NoSQL languages.
In a third, more ambitious and prospective part of the work, we expect the PhD student to model other databases functionalities with the Coq proof assistant - Extra information
- Prerequisite
- The candidate should have a very strong background in theoretical computer science with emphasis in logic as well as a concrete practical experience of functional programming in OCaml-like programming languages. A good knowledge of Coq will be a plus.
- Détails
datacert.pdf- Expected funding
- Institutional funding
- Status of funding
- Expected
- Candidates
- Stefania Dumbrava
- Utilisateur
- veronique.benzaken
- Créé
- Jeudi 01 mars 2012 15:59:00 CET
- dernière modif.
- Vendredi 01 juin 2012 16:30:47 CEST
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit
Assistante
Stéphanie Druetta
Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr