Publications in Refereed Conferences

From Traces to Proofs: Proving Concurrent Program Safe. Chinmay Narayan, Subodh Sharma, Shibashis Guha and S. Arun-Kumar. Accepted in TASE 2016.

Unfolding-based Partial Order Reduction. César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening. Accepted in CONCUR 2015. Best Paper Award.

Accelerated test execution using GPUs. Ajitha Rajan, Subodh Sharma, Peter Schrammel, Daniel Kroening ASE 2014: 97-102

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh 

Sharma FM 2014: 263-278

A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications. Subodh Sharma, Ganesh Gopalakrishnan, Greg Bronevetsky. SBMF 2012: 


MAPPED: Predictive Dynamic Analysis Tool for MPI Applications. Subodh Sharma Ganesh Gopalakrishnan, Greg Bronevetsky. SC Companion 2012: 1425-1426

Efficient Verification Solutions for Message Passing Systems. Subodh Sharma, Ganesh Gopalakrishnan. IPDPS Workshops 2011: 2026-2029

MCC: A runtime verification tool for MCAPI user applications. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt. FMCAD 2009: 41-44

Dynamic verification of Multicore Communication applications in MCAPI. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer. HLDVT 2009: 100-105

ISP: a tool for model checking MPI programs. Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, Robert M. Kirby. PPoPP 2008: 285-286

A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs. Subodh Sharma, Sarvani Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kriby, Rajeev Thakur, William Gropp. Euro MPI 2008: 265-273


  1. Mopper -- Dynamic symbolic tool to verify MPI executions.