P83: Contracts for Message-Passing Programs
Abstract: Verification 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.
Award: Best Poster Finalist (BP): no
Two-page extended abstract: pdf