Concurrent search structures: Reusable interfaces for verifying concurrent C data structures across synchronization patterns.
Compiler-facing concurrency: Connecting concurrent separation-logic proofs to CompCert Clight executions.
CCris and RefinedCC: Adding annotation-driven automation to Iris-based Clight verification.
Relaxed-memory libraries: Developed stronger specifications for Repaired C11 libraries by combining logical atomicity with enriched partial-order reasoning in Iris.
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]
Pre-UIC Publications
Foundations for Reasoning about Holistic Specifications
Duc-Than Nguyen
Master of Philosophy Thesis, University of Melbourne, Australia (2021)
[Thesis]
[Isabelle development]
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, Than Duc Nguyen, Long D. Tran
International Conference on Computational Science and Its Applications (2013)
[Paper]