Duc-Than Nguyen

I'm on the academic job market, seeking academic positions in software correctness, reliability, and security, with a focus on formal methods and verification, while also actively exploring research-oriented industry opportunities.

I'm a final-year Ph.D. candidate at the University of Illinois Chicago in the area of Programming Languages and Formal Methods, 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 develop techniques for verifying 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 sees wider adoption in academia and industry, including at Amazon and Google DeepMind, I plan to gain experience with it as well.

My doctoral research has been conducted as part of National Science Foundation–funded projects (Awards #1811894 and #2414582).

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