MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Deductive Verification of MPI Protocols
Vasco T.VASCONCELOS , Franciisco MARTINS , Eduardo R.B.MARQUES , Nobuko YOSHIDA , Nicholas NG
Behavioural Types: from Theory to Tools p. 353 - 372

This chapter presents the PARTYPES framework to statically verify C programs that use the Message Passing Interface, the widely used standard for message-based parallel applications. Programs are checked against a protocol specification that captures the interaction in an MPI program. The protocol language is based on a dependent type system that is able to express various MPI communication primitives, including point-to-point and collective operations. The verification uses VCC, a mechanical verifier for concurrent C programs. It takes the program protocol written in VCC format, an annotated version of the MPI library, and the program to verify, and checks whether the program complies with the protocol.

@article{VMMYN2017,
  author = {Vasco T. Vasconcelos and Franciisco Martins and Eduardo R.B. Marques and Nobuko Yoshida and Nicholas Ng},
  title = {{Deductive Verification of MPI Protocols}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {353--372},
  publisher = {River Publishers},
  year = 2017
}
@article{VMMYN2017,
  author = {Vasco T. Vasconcelos and Franciisco Martins and Eduardo R.B. Marques and Nobuko Yoshida and Nicholas Ng},
  title = {{Deductive Verification of MPI Protocols}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {353--372},
  publisher = {River Publishers},
  doi = "10.13052/rp-9788793519817",
  year = 2017
}