Many industrial applications, including safety-critical ones, consist of several dis- joint components that use message passing to communicate according to some protocol. These components are typically highly concurrent, since message ex- changes may occur in any order. Developing correct message passing programs is therefore very challenging, which makes proving their correctness crucial . A popular API for implementing message passing programs is the Message Passing Interface (MPI) library. We focus on the modular veri�cation of MPI programs. Related work mainly focuses on communication and considers abstract models rather than concrete implementations [10,5]. We consider concrete Java code and combine static veri�cation with well-known techniques for reasoning about concurrent and distributed programs, based on process algebras .
|Number of pages||2|
|Publication status||Published - Mar 2016|
|Event||ICT.OPEN 2016 - Amersfoort, Netherlands|
Duration: 21 Mar 2016 → 22 Mar 2016
|Period||21/03/16 → 22/03/16|