SPIKEpar : une interface parallèle du démonstrateur automatique SPIKE

Sorin Stratulat 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Nous décrivons une interface parallèle pour le démonstrateur automatique SPIKE telle qu'elle est mise en oeuvre sur un réseau de stations de travail monoprocesseur. l'approche maître-esclave abordée pour paralléliser le calcul symbolique lié aux preuves mécaniques par récurrence permet de partager la quantité de travail entre les processeurs selon le modèle de parallélisation de type ET, conforme à la stratégie. Un processus SPIKE effectue des calculs à gros grain au niveau des clauses.
Type de document :
Communication dans un congrès
RENPAR'10 : Rencontres Francophones du Parallélisme des Architectures et des Systèmes, 1998, Strasbourg, France, pp.210-213, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098701
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:17:55
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:27:49

Fichiers

Identifiants

  • HAL Id : inria-00098701, version 1

Collections

Citation

Sorin Stratulat. SPIKEpar : une interface parallèle du démonstrateur automatique SPIKE. RENPAR'10 : Rencontres Francophones du Parallélisme des Architectures et des Systèmes, 1998, Strasbourg, France, pp.210-213, 1998. 〈inria-00098701〉

Partager

Métriques

Consultations de la notice

123

Téléchargements de fichiers

27