I have worked on various research
projects/problems. Here is a list of of projects that I am currently
working on or have worked on earlier.
- Macroscopic symmetry-aware
Partial Order Reduction for MPI programs: This work is currently
under progress. We are working on a preliminary draft of the paper
which will be available soon. The idea is to explore the semantics of
MPI communication calls to develop sound heuristic to cut down the
interleaving space of an MPI program drastically. More details would be
available in the paper.
- MCC - An MCAPI verification tool:
MCC
is
an
explicit model checker to verify applications that use MCAPI
message oriented communication. It checks for the presence of deep
seated deadlocks and safety assertion violations in the application.
The MCC scheduler enforces determinism in a novel way at runtime and
exhaustively explores the relevant
execution scenarios of the program. It employs ISP's POE algorithm.
More details can be found in here.
- Functionally Irrelevant Barrier
Detection: In MPI programs people often use MPI barriers as a
good measure or for synchronization purposes. Unnecessary use of
barriers can hit the parallelism of an application and slow the runtime
of the program. We developed a sound formal algorithm built on top of ISP to detect such
functionally irrelevant barrier which are safe to be removed without
adding any new communication behaviors to the program. More details can
be found here.
I have also worked on some interesting research problems over summer
internships at various research labs.
- Symbolic analysis of Assembly
level programs (Freescale Semiconductor Inc.): Developed a
symbolic analysis engine to take an assembly program trace and convert
it into a SMT formula which when fed to a decision procedure will tell
us the feasibility of that program trace with input vector valuations.
- Automatic test case generation
for C++ programs (NEC Research Labs): Developed a framework to
take in a C++ program with a given object pool, to construct a test
case for testing out dynamic dispatch and inheritance hierarchy.
For a complete list of papers click Publications tab.