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

Sorin Stratulat

Conference papers

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

Sorin Stratulat ¹

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

Domain :

Computer Science [cs] / Other [cs.OH]

Complete list of metadata

https://hal.inria.fr/inria-00098701
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:17:55 AM
Last modification on : Friday, February 4, 2022 - 3:33:27 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:27:49 PM

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

Files

Identifiers

Collections

Citation

Export

Metrics

75

26

Contact Legal Notice Personal Data

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

Files

Identifiers

Collections

Citation

Export

Share

Metrics

75

26

Contact Legal Notice Personal Data