Duc-Than Nguyen

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

I'm a final-year Ph.D. candidate at the University of Illinois Chicago, working in programming languages and formal methods, advised by Prof. William Mansky. My research focuses on making formal verification more practical, modular, and reusable for concurrent and security-critical systems software.

In particular, I use the Verified Software Toolchain and Iris to verify realistic concurrent C programs and to develop simpler, more scalable methods for reasoning about fine-grained concurrency. I primarily use the Rocq interactive theorem prover to construct machine-checked correctness proofs. During my master’s studies, I also worked with Isabelle on formalizing holistic specifications, and I plan to gain experience with Lean as its use continues to grow in academia and industry.

See my research page and CV for more details.