An experiment in parallelizing an application using formal methods -: Computer aided parallelization

Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.