Research

Projects

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

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] [Coq Formalization] [Artifact] [Slide] [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 Languages Design and Implementation)
[Paper] [Project Page]

Foundations for Reasoning about Holistic Specifications
Duc-Than Nguyen
Master of Philosophy - Dissertation @ University of Melbourne, Australia (2021)
[PDF]
Efficient Privacy Preserving Data Audit in 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
Nguyen, Thuc D., Than Duc Nguyen, and Long D. Tran
International Conference on Computational Science and Its Applications (2013)
[Paper]

A Critique of Sequential Consistency in C11
Duc-Than Nguyen
Ph.D. Qualifier Examination 2022 @ UIC
[PDF] [Slide]