Mentee

Anastasia V. Mironova
Department of Mathematical Sciences
University of Alaska Anchorage
Education goals: B.S. Computer Science, B.S. Mathematics
Graduation date: December 2004
anastasia.mironova@gmail.com

Primary Mentor

Lori A. Clarke, Ph.D.
Laboratory for Advanced Software Engineering Research (LASER)
Department of Computer Science
University of Massachusetts at Amherst
Research interests: Analysis of concurrent software, Object management, 
Software architecture

Stephen F. Siegel, Ph.D.
George Avrunin, Ph.D.

Using Model Checking with Symbolic Execution for the
Verification of Data-Dependent Properties of MPI-Based
Parallel Scientific Software

Description

The main goal of this project is to research modeling and verification of propertied for sample
MPI-based programs using the SPIN model checker.

In particular:

• Getting a general understanding of the work in this field;
  
• Becoming familiar with the particular tools and languages necessary for conducting research,
  such as the SPIN model checker, Message Passing Interface(MPI), and C programming language;
  
• Constructing sample programs in PROMELA for performing verification using SPIN;
  
• Performing analysis on the derived PROMELA models in order to draw conclusions about efficiency and possible scalability of the defferent techniques utilized.

Project Journal

Project Presentation

Final Report

CREW/DMP Reunion event took place on October 8, 2004 in Chicago, IL and I was one of the participants, presenting a poster.

Miscellaneous Links

Picture Galleries
Gallery 1: UMass Amherst, LASER 
Gallery 2: 4th of July weekend in Boston
Gallery 3: LASER BBQ

Valerie Gartland was also a DMP student working with Lori that summer, her website is a lot of fun:
http://sol.cs.wcu.edu/~valerie/dmp/