From BSP Routines to High-performance ones: Formal Verification of a Transformation Case

Abstract. PUB (Paderborn University BSPLib) is a C library support-ing the development of Bulk-Synchronous Parallel (BSP) algorithms. We present a formal semantics that emphasises the high-performance prim-itives of the PUB. This semantics is here used to formally verify (using the Coq proof assistant) a simple optimization of the source code that transforms classical BSP routines to their high-performance versions