Skip to Main content Skip to Navigation
Theses

Utilisation des méthodes formelles pour le développement de programmes parallèles

Abstract : The goalofthework described in this thesis is to study how formaI methods can be applied to the parallelization of sequentialprograms. The use offormal methods helps to ensure that parallelization is correct. One of our objectives being towork on real applications,we havecollaborated with physicists and chemists of our University to parallelize three of their simulations. These applications have been parallelized on the Origin 2000at the Charles Hermite Centre, using either OpenMP, or MPI, or both.To prove that domain decompositiop based parallelization is correct, we have developed a method that requires the user ta make an abstraction of his/her sequentialcode in order to obtaLu a postcondition. We must then generalize. it for the parallel code. Consequently, we must prove that the postconditions of theparallelcode together with the postcondition of the code glueing
Document type :
Theses
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01747537
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:03:16 AM
Last modification on : Thursday, November 26, 2020 - 11:46:09 AM
Long-term archiving on: : Thursday, September 13, 2018 - 10:47:29 PM

File

SCD_T_2000_0001_COUTURIER.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01747537, version 1

Collections

Citation

Raphaël Couturier. Utilisation des méthodes formelles pour le développement de programmes parallèles. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2000. Français. ⟨NNT : 2000NAN10001⟩. ⟨tel-01747537⟩

Share

Metrics

Record views

81

Files downloads

840