Anshuman Mohan

Computer Science at Cornell University
Gates 349 · amohanⓐcs.cornell.edu

I am a first-year PhD student at Cornell Computer Science. My research is in programming languages.

Before Cornell, I was a research assistant for Aquinas Hobor. I contributed mostly to CertiGraph, a Coq development that facilitates the formal verification of graph-manipulating programs written in C. Highlights include the verification of a garbage collector for the CertiCoq compiler, the discovery of an overflow bug in Dijkstra's algorithm, and a refinement in the precondition of Prim's algorithm.

Before Aquinas, I was part of the amazing inaugural cohort of Yale-NUS College. I gave the commencement address for my graduating class.

Publications

Functional Correctness of C Implementations of Dijkstra's, Prim's, and Kruskal's Algorithms
Mohan, Leow, Hobor

CAV 2021, Online

We extend the CertiGraph library to enable reasoning about labeled edges and undirected graphs, and use it to verify C implementations of Dijkstra's, Prim's, and Kruskal's algorithms. Each of these classic algorithms has been used and studied for more than 60 years, and yet our verification reveals remarkable subtleties. We show that Dijkstra has an overflow issue that places delicate restrictions on the maximum allowable path cost. We also debunk the universal misconception that Prim runs correctly only on connected graphs. Our proofs are checked in Coq.

Functional Proof Pearl: Inverting the Ackermann Hierarchy
Tran, Mohan, Hobor

CPP 2020, New Orleans

The Ackermann function $$\mathcal{A}$$ grows explosively, and its inverse $$\alpha$$ is of interest in CS. Sadly, the standard practice of computing $$\alpha$$ via $$\mathcal{A}$$ is untenable. We give a new and efficient computation of $$\alpha$$. We also give efficient computations for the related and better-known hyperoperation hierarchy ($$+$$, $$\times$$, exp, tetration, etc) and its inverse ($$-$$, $$\div$$, log, log$$^{*}$$, etc). Our definitions are proved correct in Coq, and our time bounds are supported by pen-and-paper proofs and benchmarks after extraction to OCaml.

Certifying Graph-Manipulating C Programs via Localizations within Data Structures
Wang, Cao, Mohan, Hobor

OOPSLA 2019, Athens

Formally verifying graph algorithms is hard: nodes can be shared arbitrarily, so uninvolved subgraphs cannot be "framed away". We address this with a new separation logic rule called localize. We develop CertiGraph, a Coq library that provides a setup for defining mathematical graphs in Coq, laying them out in memory via separation logic, and stating and proving properties about them. We demonstrate the power of CertiGraph by using it to verify 7 graph-manipulating C programs. Our flagship example is a generational garbage collector. We identify two places where the semantics of C is too restrictive to define OCaml-style GCs. Our proofs are checked in Coq.

Presentations

A Verified Garbage Collector for Gallina
APLAS NIER 2019, Bali
MPI-SWS, Kaiserslautern
University of Colorado, Boulder

CertiCoq compiles Gallina into C; the transition from an infinite heap to a finite one is supported by garbage collection at the C level. We get into the weeds of the verfication of this GC, showing how the correctness property—a form of graph isomorphism—is broken and restored. We note two places where the semantics of C is too restrictive to define the behavior we need. We suspect these issues will hinder future verifications of OCaml-style GCs.

Verified Dijkstra in C
APLAS SRC 2019, Bali

We identify and explain an overflow bug in Dijkstra's algorithm. The precise bound in the relevant precondition is nontrivial: we show that the intuitive guess fails, and provide a workable refinement. We demonstrate the bug and our fix with Coq proofs. This work was developed into our CAV 2021 paper.

Service

External Reviewer

ESOP 2020

Personal

A (working) list of the eight best things I have consumed recently

My favorite novels have long been Catch-22 and The God of Small Things, which worked nicely as a tragicomedy soup. Sometimes a Great Notion has recently entered the mix; the implications of this are unclear. If You Have to be a Floor is a truly special podcast episode, while This is Chance is a story I'd consume in any medium. You Want It Darker is a good song and The Last Emperor is a good movie. My friends and I made tacos with carnitas, mango salsa, and duckfat tortillas last year, and those too were good.

To plant a garden do scientific research is to believe in tomorrow

The point of doing science is to have your work seen, used, and made redundant. Sadly, at the rate we're heating the planet, we'll soon have more rudimentary things to worry about. I'm cautiously optimistic about climate change, but with the understanding that intentional work is needed from everyone who can afford to put it in. I'm still working on my plan, so please reach out if you'd like to discuss this as either a mentor or a coconspirator.