Anshuman Mohan

Computer Science at
NUS

yncmaⓐcomp.nus.edu.sg

Starting in January 2020, I will be a **PhD student at Cornell
Computer Science**.

I am currently a research assistant for
Aquinas Hobor.
Our research is in programming languages, and our main project is a Coq development that eases the **formal
verification** of graph-manipulating programs written in C.
Fun highlights include a verified garbage collector for the
CertiCoq compiler and the discovery of a bug in Dijkstra'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 and currently serve on the Alumni Council.

Publications

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 benchmarked after extraction to OCaml.

Certifying Graph-Manipulating C Programs
via Localizations within Data Structures

Wang, Cao, Mohan, Hobor
OOPSLA 2019, Athens

The formal verification of 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, develop an extensible Coq library to further ease verifications, and use the library to verify seven 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. In two places, we find that the semantics of C is too restrictive to define the behavior we need. We suspect these restrictions will hinder future verifications of OCaml-style GCs.

We identify and explain an overflow bug in Dijkstra's classic 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 its fix with Coq proofs. A paper about this result is under preparation.

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 philosophical implications of this are as yet unclear. If You Have to be a Floor is a truly special podcast episode, while This is Chance! is an amazing story that I'd consume in any medium. A bowl of gudeg I had in Yogyakarta early this year is the best food I can remember. You Want It Darker is a good song and The Last Emperor is a good movie.

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

Part of the point of doing science is to have your work seen, used, and eventually made redundant. Sadly, at the rate we're heating the planet, we will soon have more rudimentary things to worry about. I am 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.