Seminar by Subodh Sharma
Precise and Scalable Dynamic Predictive Analysis of Distributed Software
Subodh Sharma
Oxford University, UK
Date: Friday, August 22nd, 2014
Time: 3:00 PM
Venue: RM101.Abstract:
The scheduling nondeterminism in distributed software can lead to divergent behavior that is hard to reproduce. Therefore, formal verification of distributed software becomes indispensable in such situations. In this talk, I first present a dynamic formal verification (i.e. combination of model-checking and testing) technique for distributed software which is developed using MPI (a popular message passing standard which, by many, is considered the lingua-franca of high performance computing software). While being precise and effective in discovering defects, dynamic verification of distributed software scales only to a few processes. To address this issue of scalability while maintaining precision, I will then present a hybrid approach that leverages an efficiently engineered SAT technology coupled with our dynamic verification technique. Finally, I will end my talk with future research directions in the area.
About the speaker:
Subodh Sharma is a Post-doctoral fellow in the Department of Computer Science at the University of Oxford. He obtained his Ph.D. in 2012 from the University of Utah during which he worked on verifying high performance computing software written using MPI. His current research interests lie in the area of concurrent program verification via a synergistic use of static and dynamic analysis.