Describir: Formal analysis of MPI-based parallel programs.