Duc-Than Nguyen

• VST & concurrency: Extended the VST soundness proof and program logic to support concurrency, atomic operations, and weak-memory reasoning.
• CCris: Built an annotation-based verification framework on top of VST using RefinedC.
• Concurrent Search Structure Templates: Implemented template-based verification techniques in VST and applied them to prove the correctness of fine-grained concurrent search structure implementations in C.
• Specifications for Relaxed Libraries in Iris: Developed stronger specifications for relaxedmemory libraries by combining logical atomicity with enriched partial-order reasoning, targeting the weaker memory model of Repaired C11 and building on top of the Iris framework.

>>> Google Scholar

• A Formal Interface for Concurrent Search Structure Templates
  Duc-Than Nguyen, William Mansky
  ESOP 2026 (European Symposium on Programming)
  [Paper] [Rocq development] [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] [Rocq development] [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]