Abhishek Kr Singh

Parallel computing matters more than ever under AI-driven load, yet parallel programming stays difficult because the weak memory models beneath modern architectures (x86-TSO, POWER, ARM, RISC-V) and languages (C11, RC11) behave unintuitively. Despite decades of work on concurrency semantics, reasoning about concurrent code remains out of reach for most programmers. This project develops largely automated mechanisms for establishing trust in parallel programs, combining program semantics, automated theorem proving, model checking, testing, and fuzzing.

Generative AI has changed how software gets written: a developer describes what they want in plain language and a model produces code. But natural language is ambiguous, so intent can be misread and the resulting program can quietly diverge from the real goal, with no practical way to guarantee functional correctness without human oversight. This project builds frameworks that bridge informal descriptions and rigorous formal specifications, so programmer intent can be stated precisely and AI-generated code verified as part of the development lifecycle rather than trusted on inspection.

Proof assistants have produced remarkable high-assurance software — CompCert, seL4, CakeML — yet formal development stays outside the mainstream, largely because writing and maintaining verified specifications demands so much human effort. This project applies machine learning to cut that cost: making proof search more efficient, automating tactic selection during proof completion, and predicting the hypotheses and intermediate lemmas that carry a proof forward.

Navigation Among Movable Obstacles asks a robot to reach a goal in a cluttered space where it may push, pull, or carry objects out of the way. Because the robot changes the environment as it acts, the search space grows with every object it is allowed to touch. This project looks for planners that come with guarantees rather than empirical success rates: completeness under stated assumptions.