Dr Subodh Sharma
My broad goal is to use automated verification techniques to ensure software reliability and security. My primary interests lie in the verification of concurrent and distributed programs via static/dynamic analysis and model checking.
I am currently a post-doctoral research assistant in the Systems Verification group headed by Prof. Daniel Kroening since April, 2012. I finished my Ph.D. from the University of Utah under the supervision of Prof. Ganesh Gopalakrishnan in March, 2012. During my PhD I studied the problem of verifying message passing software (written using MPI and MCAPI) via dynamic verification methods. My on-going work here in Oxford is focused on exploring symbolic based methods to assist dynamic verification thereby allowing scalable verification of message passing software.
The paper "Unfolding-based Partial Order Reduction" won the best paper award at CONCUR 2015
Precise Predictive Analysis for Discovering Communication Deadlocks in Message Passing Programs
Vojtech Forejt‚ Daniel Kroening‚ Ganesh Narayanswamy and Subodh Sharma
In FM 2014: Formal Methods. Vol. 8442 of Lecture Notes in Computer Science. Pages 263−278. Springer International Publishing. 2014.
Abstract: MAPPED: Predictive Dynamic Analysis Tool for MPI Applications
S. Sharma‚ G. Gopalakrishnan and G. Bronevetsky
In High Performance Computing‚ Networking‚ Storage and Analysis (SCC)‚ 2012 SC Companion:. Pages 1425–1426. November, 2012.
A Sound Reduction of Persistent−Sets for Deadlock Detection in MPI Applications
Subodh Sharma‚ Ganesh Gopalakrishnan and Greg Bronevetsky
In Rohit Gheyi and David Naumann, editors, Formal Methods: Foundations and Applications. Pages 194–209. Springer Berlin Heidelberg. January, 2012.