Verification of parallelized Stencils based on data dependence analysis

  • Context: Stencils are a class of algorithms in which the value of a matrix cell is computed based on the value of the neighboring cells. As they are usually run on huge matrices these algorithms run on sub-matrices in parallel to gain better performance. Often, there is no guarantee that at the synchronization points between different cores, cell values are passed in the correct order.


    Goal: Formal verification of a parallelized stencil to make sure that the data dependences implied by the stencil are not broken by parallelization.


    Prerequisites: Understanding of formal verification (at the level of Formale Systeme 1 course)