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.

Currently, I am 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 using the Isabelle to formalize holistic specifications. As the Lean Proof Assistant gains broader adoption among mathematicians, computer scientists, and industry leaders such as Amazon and Google DeepMind, I plan to gain experience with it.

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