Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Research Actions at LIFO > Research Action : PROPAC

Site en Français



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37



PROPAC : Certified Parallel Programming

The goals of this project is to produce a programming environment in which certified parallel programs can be written, proved and safely executed.

More technically, several subgoals will be studied to achieve the overall goal of the project:

  • Proofs, using the Coq proof assistant, of programs written with the functional parallel languages we developped.
  • Certification of the compilers for these languages, from source code to bytecode for parallel virtual machines and the certification of these virtual machines
  • Proofs of imperative bulk synchronous parallel programs first written with a small dedicated language and then with an extension of C or Java.
  • Automatic performance prediction of the programs written with these languages.

Funding

French Ministry of Research, Young Researchers Program

Participating Members

Radia BENHEDDI

Frédéric LOULERGUE

Action's Web Page

http://wwwpropac.free.fr/