Dans cet article nous décrivons la parallélisation d'une application développée par des physiciens. Les calculs sont réalisés par un nombre important d'itérations courtes dépendantes les unes des autres. Pour paralléliser cette application, nous découpons la grille représentant le système physique en plusieurs sous-grilles et nous regroupons les différents calculs obtenus. Nous avons prouvé à l'aide de PVS (Prototype Verification System) que cette parallélisation est correcte ; pour ce faire nous faisons une abstraction du programme par l'intermédiaire d'une spécification du prouveur PVS. Finalement nous expliquons comment PVS nous permet de trouver la post-condition nécessaire afin de coller les différentes sous-grilles pour garantir que le calcul parallèle est identique au calcul séquentiel.