This subject has been submitted as part of an International ANR project with Portugal.
Principal Investigators are
Jean-Christophe Filliâtre (CNRS, LRI)
Simão Melo de Sousa (LIACC, Portugal)
Benjamin Monate (CEA LIST)
Abstract
This thesis is part of a project to design a language and proof environment for reasoning on distributed programs. The goal is to build formally proved versions of largely used libraries for parallel programming such as MPI or map-reduce primitives.
One of the objectives will be to design appropriate libraries of functions, specification and proof techniques to handle a message passing style of programming.
Context
Objectives
Work program
Primitives for distributed computing are based on specific protocols for communication, synchronisation and the combination of the results of computation. A number of key constructions will be selected typically from the standard MPI library and the Functory library developed at LRI. Their specifications will be given in a modular and parametric way taking advantage of the high-level specification language. Data types used in the protocol and the network topology will be treated as abstract notions. This specification should both be suitable for proving programs running on top of these
protocols (like high-performance algorithms) and also adapted to the verification tools developed in the project. In parallel to the specification and proof of the abstract version of the protocols used in the libraries, a challenge is to be able to actually fully prove C implementations of some of them.
Extra information
Prerequisite
Détails
Expected funding
Research contract
Status of funding
Expected
Candidates
Utilisateur
christine.paulin
Créé
Dimanche 08 avril 2012 08:55:54 CEST
dernière modif.
Dimanche 08 avril 2012 08:55:54 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
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