Duc-Than Nguyen

Projects

  • VST & concurrency: Extend VST's soundness proof and logic to support concurrency, atomic operations, and weak memory
  • CCris: Build an annotation-based proof tool on top of VST using the RefinedC framework
  • Verification of Concurrent C Programs with Search Structure Templates
  • Developing specifications for Relaxed libraries, built on top of Iris

Research Papers

>>> Google Scholar

  • A Formal Interface for Concurrent Search Structure Templates
    Duc-Than Nguyen, William Mansky
    To appear at ESOP 2026 (European Symposium on Programming)
    [Paper] [Artifact]
  • Compositional Verification of Concurrent C Programs with Search Structure Templates
    Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang
    CPP 2024 (ACM SIGPLAN International Conference on Certified Programs and Proofs)
    [Paper] [Artifact] [Video]
  • Compass: Strong and Compositional Library Specifications in Relaxed-Memory Separation Logic
    Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer
    PLDI 2022 (ACM SIGPLAN Conference on Programming Language Design and Implementation)
    [Paper] [Project Page]

Pre-UIC Publications

  • Foundations for Reasoning about Holistic Specifications
    Duc-Than Nguyen
    Master of Philosophy Thesis, University of Melbourne, Australia (2021)
    [Thesis]
  • Efficient Privacy-Preserving Data Audit in the Cloud
    Hai-Van Dang, Thai-Son Tran, Duc-Than Nguyen, Thach V. Bui, Dinh-Thuc Nguyen
    Advanced Computational Methods for Knowledge Engineering (2015)
    [Paper]
  • Attacks on Low Private Exponent RSA: An Experimental Study
    Thuc D. Nguyen, Duc-Than Nguyen, Long D. Tran
    International Conference on Computational Science and Its Applications (2013)
    [Paper]