Duc-Than Nguyen

I'm a Ph.D. candidate in Computer Science at the University of Illinois Chicago, advised by Prof. William Mansky. My primary research interest lies in advancing provably correct software, with a focus on developing and applying formal verification techniques for concurrent programs. In particular, I am developing techniques to verify the correctness of concurrent C programs using the Verified Software Toolchain and Iris, with the goal of proving the correctness of realistic systems-level concurrent code and developing simpler, more scalable approaches to reasoning about fine-grained concurrency.

I primarily use the Rocq interactive theorem prover to develop and mechanize machine-checked correctness proofs. During my master's studies, I also gained experience with Isabelle for formalizing holistic specifications. As the Lean Proof Assistant continues to gain broader adoption in both academia and industry—including organizations such as Amazon and Google DeepMind—I plan to gain experience with it as well.

My current research is supported in part by the National Science Foundation (NSF) under awards #1811894 and #2414582.

You can find details about my projects and publications on the research page, and my CV is available here.