Skip to Main content Skip to Navigation
Conference papers

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.
Mots-clés : calcul symbolique parallèle coarse-grain parallelism parallel symbolic computations rewriting systems inductive theorem proving SPIKE systèmes de réécriture démonstration de théorèmes par récurrence parallélisme à gros grain
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00098701
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:17:55 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:27:49 PM

Files

Vignette du document
98-R-138.pdf

Identifiers

  • HAL Id : inria-00098701, version 1

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE

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. ⟨inria-00098701⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

149

Files downloads

67

 

Contact                    Legal Notice                    Personal Data