Static Verification of Message Passing Programs

Wytse Hendrikus Marinus Oortwijn, Stefan Blom, Marieke Huisman

    Research output: Contribution to conferencePaper

    151 Downloads (Pure)

    Abstract

    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 [4]. 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 [7].
    Original languageUndefined
    Number of pages2
    Publication statusPublished - Mar 2016
    EventICT.OPEN 2016 - Amersfoort, Netherlands
    Duration: 21 Mar 201622 Mar 2016

    Conference

    ConferenceICT.OPEN 2016
    CountryNetherlands
    CityAmersfoort
    Period21/03/1622/03/16

    Keywords

    • IR-104115
    • EWI-27674

    Cite this

    Oortwijn, W. H. M., Blom, S., & Huisman, M. (2016). Static Verification of Message Passing Programs. Paper presented at ICT.OPEN 2016, Amersfoort, Netherlands.