P83: Contracts for Message-Passing Programs
SessionPoster Reception
Authors
Event Type
ACM Student Research Competition
Poster
Reception
TimeTuesday, November 14th5:15pm -
7pm
LocationFour Seasons Ballroom
DescriptionVerification of message-passing parallel programs is
challenging because of the state-explosion problem. A
procedure-level contract system for parallel programs
can help overcome this challenge by verifying contracts
individually, in a modular way. A contract system is
used to specify intended behaviors of programs.
Contracts can be checked at run-time or verified
formally. There is a mature theory of contracts for
sequential programs, but little work has been done on
parallel programs, and even less for message-passing
parallel programs. We developed a theory of contracts
for message-passing programs and realize this theory in
a contract language for programs that use the Message
Passing Interface (MPI). We are also developing a
verification tool that uses symbolic execution and model
checking techniques to prove that MPI programs satisfy
their contracts.
