Subodh Sharma



Refereed Publications

(Copyrights belong to the publishers)

2017

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. ACM TOPLAS 2017. [Bib]
V. Forejt, S. Joshi, D. Kroening, G. Narayanaswamy, S. Sharma.

Privacy and Security of Aadhaar: A Computer Science Perspective. Economic & Political Weekly 2017. [Bib]
S. Agrawal, S. Banerjee, S. Sharma.

2016

Pollux: Safely Upgrading Dependent Application Libraries. FSE 2016. [Bib]
S. Kalra, A. Goel, D. Khanna, M. Dhawan, S. Sharma, R. Purandare.

From Traces to Proofs: Proving Concurrent Programs Correct. TASE 2016. [Bib]
C. Narayan, S. Sharma, S. Guha, S.A. Kumar.

2015

Unfolding-based Partial Order Reduction. CONCUR 2015 (Best Paper Award). [Bib]
C. Rodriguez, M. Sousa, S. Sharma, D. Kroening.

2014

Accelerated test execution using GPUs. ASE 2014. [Bib]
A. Rajan, S. Sharma, P. Schrammel, D. Kroening.

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. FM 2014. [Bib]
V. Forejt, D. Kroening, G. Narayanaswamy, S. Sharma.

2012

A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications. SBMF 2012. [Bib]
S. Sharma, G. Gopalakrishnan, G. Bronevetsky.

MAPPED: Predictive Dynamic Analysis Tool for MPI Applications. SC Companion 2012. [Bib]
S. Sharma, G. Gopalakrishnan, G. Bronevetsky.

2011

Efficient Verification Solutions for Message Passing Systems. IPDPS Workshops 2011. [Bib]
S. Sharma, G. Gopalakrishnan.

2009

Dynamic verification of Multicore Communication applications in MCAPI. HLDVT 2009. [Bib]
S. Sharma, G. Gopalakrishnan, E. Mercer.

Some resources for teaching concurrency. PADTAD 2009. [Bib]
G. Gopalakrishnan, Y. Yang, S. Vakkalanka, A. Vo, S. Aananthakrishnan, G. Szubzda, G. Sawaya, J. Williams, S. Sharma, M. Delisi, S. Atzeni.

MCC: A runtime verification tool for MCAPI user applications. FMCAD 2009. [Bib]
S. Sharma, G. Gopalakrishnan, E. Mercer, J. Holt:

2008

ISP: a tool for model checking MPI programs. PPoPP 2008. [Bib]
S. Vakkalanka, S. Sharma, G. Gopalakrishnan, R. M. Kirby.

A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs. EuroPVM/MPI 2008. [Bib]
S. Sharma, S. Vakkalanka, G. Gopalakrishnan, R. M. Kirby, R. Thakur, W. Gropp.

Tools

Mopper

Verifies whether an MPI C trace is free of communication deadlocks

Pollux

A binary analysis tool built over Intel's PIN instrumentation framework to detect semantic similarity across 3rd party library upgrades. (Code available upon request).