Aayushi Gautam

DPOR-Guided Fuzzing for Multithreaded Programs

Antithesis — Summer 2026

• Integrated DPOR-based model checking into a fuzzer to guide trace prioritization, deprioritizing directions that fall in the same equivalence class.
• Delivered a complete implementation for multithreaded programs, reducing redundant exploration in concurrency testing.

Formal Verification of MPI Message Semantics

Max Planck Institute for Software Systems — Spring 2026

• Formalized MPI's message-matching and ordering rules as a precise mathematical model and proved correctness against the official specification.
• Identified and corrected a gap in an existing distributed-systems verification framework's treatment of wildcard receive operations.
• Extended the framework to support MPI-specific features (source/tag wildcards, multiple channels) with proof-backed justification for each design choice.
• Verified that new rules preserved the framework's core guarantees of correctness, completeness, and efficiency.

DeepDebugging (Ongoing)

Developing a debugging methodology that combines DMTCP checkpointing with McMini model checking to efficiently diagnose concurrency bugs in multithreaded applications.

Transparently Checkpointing CUDA on GPUs

Developed a low-latency checkpointing system for NVIDIA GPUs using CUDA Runtime API and Unified Memory, enabling fault tolerance for HPC workloads on the Perlmutter supercomputer.

DMTCP for RISC-V

Extended DMTCP to RISC-V architectures using the GCC cross-compilation toolchain. Work presented at Latch-Up 2024.

Mini Model Checker

A bounded stateless explicit-state model checker for finding deadlock and assertion errors in multithreaded software.

Research Intern

Visiting Scholar

Research Intern

Research Intern

Senior Project Technical Assistant