Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches

Loulergue, Frédéric ; Robillard, Simon ; et al.

In: Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL) ; https://hal.inria.fr/hal-00979092 ; Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014, Paris, France, 2014

Konferenz

Wie komme ich dran?

National audience ; Le problème des valeurs inférieures les plus proches est un problème important pour la programmation parallèle car il peut être utilisé pour résoudre plusieurs problèmes plus spécifiques et est l'une des phases d'algorithmes plus complexes. Avec l'assistant de preuve Coq, nous développons formellement par construction un programme parallèle fonctionnel pour résoudre ce problème, en utilisant la théorie des homomorphismes parallèles quasi synchrones. Les performances du programme parallèle fonctionnel obtenu par extraction sont comparées avec une version dérivée sans support logiciel et implantées avec la bibliothèque C++ de squelettes algorithmiques OSL, et avec une implantation d'un algorithme non vérifié du à He et Huang.

Titel:	Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches
Autor/in / Beteiligte Person:	Loulergue, Frédéric ; Robillard, Simon ; Tesson, Julien ; Legaux, Joeffrey ; Hu, Zhenjiang ; Laboratoire d'Informatique Fondamentale d'Orléans (LIFO) ; Ecole Nationale Supérieure d'Ingénieurs de Bourges-Université d'Orléans (UO) ; Laboratoire d'Algorithmique Complexité et Logique (LACL) ; Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Centre National de la Recherche Scientifique (CNRS) ; Université d'Orléans (UO)-Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA) ; Center, GRACE ; National Institute of Informatics (NII) ; Information Processsing Laboratory (IPL) ; The University of Tokyo (UTokyo) ; ANR-10-INTB-0205,PAPDAS,Developpement de programmes parallèles avec des squelettes algorithmiques(2010)
Link:	https://hal.inria.fr/hal-00979092
Zeitschrift:	Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL) ; https://hal.inria.fr/hal-00979092 ; Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014, Paris, France, 2014
Veröffentlichung:	HAL CCSD, 2014
Medientyp:	Konferenz
Schlagwort:	Paris France programmation parallèle programmation fonctionnelle transformation de programmes assistant de preuve [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Subject Geographic: Paris France
Sonstiges:	Nachgewiesen in: BASE Sprachen: French Collection: Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) Document Type: conference object Language: French Relation: hal-00979092; https://hal.inria.fr/hal-00979092

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.