Skip to main content

Taming Schedule Space Explosion in Message Passing Application Verification

Subodh Sharma ( University of Oxford )

Message passing (MP) has gained a widespread adoption over the years. Traditionally, message passing has been employed in the application construction specifically meant for high performance computing, however, this is not true anymore. We are witnessing quite a shift in computing practices with message passing serving a much larger audience than ever before. With such growing importance, it becomes essential to have formal tools and methodologies to establish correctness of MP applications. While there has been some state-of-the-art verifiers and methodologies for MP applications, they all suffer from a common problem: schedule-space explosion! In this talk, I will present and discuss two strategies to effectively contain the schedule-space explosion. These strategies are specifically meant for dynamic verification engines which operate in a closed environment (i.e. for a fixed input). I would further discuss the soundness and completeness aspects of these strategies and their ability to verify practical MP applications in a scalable manner.

Speaker bio

Subodh Sharma is a Post-Doctoral research assistant in the Department of Computer Science at the Oxford University. Early this year, he defended his PhD in the area of dynamic verification of message passing applications from the University of Utah. His broader research interests lie in the domain of concurrent program verification via static-dynamic program analysis, model checking, and theorem proving.



Share this: