Static Verification of Message Passing Programs

Research output: Contribution to conferencePaper

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].
LanguageUndefined
Number of pages2
StatePublished - 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.
Oortwijn, Wytse Hendrikus Marinus ; Blom, Stefan ; Huisman, Marieke. / Static Verification of Message Passing Programs. Paper presented at ICT.OPEN 2016, Amersfoort, Netherlands.2 p.
@conference{8ef361ba9cb749f68e513804db197549,
title = "Static Verification of Message Passing Programs",
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].",
keywords = "IR-104115, EWI-27674",
author = "Oortwijn, {Wytse Hendrikus Marinus} and Stefan Blom and Marieke Huisman",
note = "extended abstract for ICT.Open; null ; Conference date: 21-03-2016 Through 22-03-2016",
year = "2016",
month = "3",
language = "Undefined",

}

Oortwijn, WHM, Blom, S & Huisman, M 2016, 'Static Verification of Message Passing Programs' Paper presented at ICT.OPEN 2016, Amersfoort, Netherlands, 21/03/16 - 22/03/16, .

Static Verification of Message Passing Programs. / Oortwijn, Wytse Hendrikus Marinus; Blom, Stefan; Huisman, Marieke.

2016. Paper presented at ICT.OPEN 2016, Amersfoort, Netherlands.

Research output: Contribution to conferencePaper

TY - CONF

T1 - Static Verification of Message Passing Programs

AU - Oortwijn,Wytse Hendrikus Marinus

AU - Blom,Stefan

AU - Huisman,Marieke

N1 - extended abstract for ICT.Open

PY - 2016/3

Y1 - 2016/3

N2 - 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].

AB - 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].

KW - IR-104115

KW - EWI-27674

M3 - Paper

ER -

Oortwijn WHM, Blom S, Huisman M. Static Verification of Message Passing Programs. 2016. Paper presented at ICT.OPEN 2016, Amersfoort, Netherlands.