Skip to Main content Skip to Navigation
New interface

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 :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:03:16 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Thursday, September 13, 2018 - 10:47:29 PM


Files produced by the author(s)


  • HAL Id : tel-01747537, version 1



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⟩



Record views


Files downloads