ABSTRACT. Many complex applications which have to tackle simulation and data analysis are a prerogative to High-Performance Computing. And so, high data volumes and performance requirements have held the parallel community developers with a clasp to deliver scalable, accurate, and most importantly bug-free solutions. Message Passing (MP) is a prominent programming model via which nodes of a distributed system communicate. Writing correct and bug-free parallel programs are hard because the participating entities interact in such non-deterministic ways that are difficult to anticipate before-hand. Programmers have to predict messaging patterns, perform data marshaling and compute locations for coordination in order to design correct and efficient programs. Unfortunately, there is a shortage of verification and formal-method techniques that can guarantee the development of correct solutions.