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 the field of provably correct software. My work focuses on programming language semantics and program correctness, with particular emphasis on concurrent systems.

I am currently developing techniques to verify the correctness of concurrent C programs using the Verified Software Toolchain and Iris. My goal is to prove the correctness of realistic concurrent systems code and to develop simpler approaches to reasoning about fine-grained concurrency.

I primarily use the Rocq interactive theorem prover to develop and mechanize 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.