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.
