πŸ“” CONTENTS
News
People
Awards
Teaching
Research
Software
Publications
Miscs
Thanks!
Contact

ROARS πŸ¦– Lab @ GMU

AI-generated DinoROARS Mascot

Welcome to ROARS (Research on Automated Reasoning Systems) Lab at George Mason University. We design and build software analysis tools with automated reasoning at their core. See Research for more information.

News

Older News

People

Lab activities/photos

Alumni
Join us: Interested in our research in safe and robust AI and software analysis?

Awards

Press Release
  1. Amazon Research Award Win for AI Safety Verification: GMU press release on the ARA
  2. Boom crash: Mason researcher receives half million NSF grant that could steer AI safely: GMU press release on CAREER award
  3. TiαΊΏn sΔ© gα»‘c Việt được tΓ i trợ nghiΓͺn cα»©u AI: from Thanh Nien, a Vietnamese news outlet
  4. CRII Award: UNL press release on NSF CRII award
  5. UNL press release on ACM SIGSOFT 10-year Most Influential Paper Award at ICSE

Teaching

Previous

Research

Software Engineering; Formal Methods; Programming Languages; Automated Reasoning; Program Analysis; Program Verification; Dynamic and Static Analysis; SMT/SAT Solving

Software

More

Publications

Google Scholars for Roars

Miscs Writing

  1. πŸ“š A book to help international students demystify and navigate the Ph.D. admission process in Computer Science in the US
  2. πŸ“ https://go.gmu.edu/cs-stats: Useful Stats about GMU CS dept
  3. πŸ“ https://go.gmu.edu/viet-cs-profs-us: Vietnamese professors in CS

Unpublished/Under Submission

  1. Hai Duong, ThanhVu Nguyen, Matthew Dwyer, A DPLL(T) Framework for Verifying Deep Neural Networks, Arxiv
  2. Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos, Eric Koskinen, ThanhVu Nguyen, DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing, Arxiv

Published/To-appear Papers

  1. Stefania Piciorea and Thanhvu Nguyen. Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code. ISSTA-Tool Demo, 2025
  2. Linhan Li and ThanhVu Nguyen. COOLer: A Language Support Extension for COOL in VS Code. ISSTA-Tool Demo, 2025
  3. Hai Duong, ThanhVu Nguyen, Matthew Dwyer. NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks. Computer Aided Verification (CAV), 2025
  4. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. The Evolution of Automated Software Repair. Transactions on Software Engineering (TSE), 2025
  5. Long Doan and ThanhVu Nguyen. AI-Assisted Autoformalization of Combinatorics Problems in Proof Assistants. International Conference on Software Engineering- New Idea and Emergining Results (ICSE-NIER), 2025
  6. Hai Duong, Dong Xu, ThanhVu Nguyen, Matthew Dwyer. Harnessing Neuron Stability to Improve DNN Verification, Foundations of Software Engineering (FSE). 859--881, 2024
  7. Didier Ishimwe. Inferring Complexity Bounds from Recurrence Relations. Foundations of Software Engineering (Student Research Competition). 2023
  8. Tung Dao, Na Meng, and ThanhVu Nguyen. Triggering Modes in Spectrum-Based Multi-Location Fault Localization, Foundations of Software Engineering (FSE) Industry Track. 1774--1785, 2023
  9. ThanhVu Nguyen and Hai Duong. NeuralSAT: A CDCL-based constraint solving approach to DNN Verification. SIGBED Blog, 2023
  10. Quoc-Sang Phan, KimHao Nguyen, ThanhVu Nguyen. Challenges in Shift Left Static Analysis, International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), 340--342, 2023
  11. Guangjing Wang, Nikolay Ivanov, Bocheng Chen, Qi Wang, ThanhVu Nguyen, Qiben Yan, Graph Learning for Interaction Analysis in Smart Home Rule Data, ACM SIGMOD,1--27, 2023
  12. SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias. ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications, Automated Software Engineering (ASE), pages 1--13, 2022
  13. Guolong Zheng, ThanhVu Nguyen, SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri. ATR: Template-based Repair for Alloy Specifications, International Symposium on Software Testing and Analysis (ISSTA), pages 666--677, 2022
  14. KimHao Nguyen, ThanhVu Nguyen, and Quoc-Sang Phan. Analyzing the CMake Build System. International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), pages 27--28, 2022
  15. Thanh-Dat Nguyen, Thanh Le Cong, ThanhVu Nguyen, Bach Le, and Huynh Quyet Thang. Toward the Analysis of Graph Neural Network. International Conference on Software Engineering- New Idea and Emergining Results (ICSE-NIER), pages 116–-120, 2022
  16. Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen. Dynaplex: Inferring Asymptotic Runtime Complexity of Recursive Programs. International Conference on Software Engineering- Tool Demo, pages 61--64, 2022
  17. ThanhVu Nguyen, KimHao Nguyen, and Hai Duong. SymInfer: Inferring Numerical Invariants using Symbolic States. International Conference on Software Engineering-Tool Demo, pages 197--201, 2022
  18. Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen. Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations, Proc. ACM Program. Lang. (OOPSLA), pages 1--23, 2021
  19. ThanhVu Nguyen, KimHao Nguyen, Matthew Dwyer. Using Symbolic States to Infer Numerical Invariants, Transactions on Software Engineering (TSE), 2021
  20. KimHao Nguyen and ThanhVu Nguyen. GenTree: Using Decision Trees to Learn Interactions for Configurable Software. International Conference on Software Engineering (ICSE), pages 1598–-1609, 2021. Artifact Evaluation
  21. Guolong Zheng, ThanhVu Nguyen, SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri, FLACK: Counterexample-Guided Fault Localization for Alloy Models, International Conference on Software Engineering (ICSE), pages 637-–648, 2021. Artifact Evaluation
  22. SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias. Bounded Exhaustive Search of Alloy Specification Repairs, International Conference on Software Engineering (ICSE), pages 1135–-1147, 2021. Artifact Evaluation
  23. KimHao Nguyen and ThanhVu Nguyen. GenTree: Inferring Configuration Interactions using Decision Trees. Automated Software Engineering (ASE Tool paper), 2021.
  24. Guolong Zheng, ThanhVu Nguyen, SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri, FLACK: Localizing Faults in Alloy Models, Automated Software Engineering (ASE Tool paper), 2021.
  25. SimΓ³n GutiΓ©rrez Brida, GermΓ‘n Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias. BeAFix: An Automated Repair Tool for Faulty Alloy Models, Automated Software Engineering (ASE Tool paper), 2021.
  26. Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. DynamiTe: Dynamic Termination and Non-termination Proofs. Proc. ACM Program. Lang. (OOPSLA), vol 4, pages 1–30, 2020.
  27. ThanhVu Nguyen, Didier Ishimwe, Alexey Malyshev, Timos Antonopoulos, and Quoc-Sang Phan. Using Dynamically Inferred Invariants to Analyze Program Runtime Complexity. Foundations of Software Engineering, Workshop on Software Security from Design to Deployment (FSE SEAD), pages 11–14, 2020.
  28. Guolong Zheng, Hamid Bagheri and Thanhvu Nguyen. Debugging Declarative Models in Alloy. International Conference on Software Maintenance and Evolution, Doctoral Symposium (ICSME), pages 844–848, 2020.
  29. ThanhVu Nguyen and KimHao Nguyen. Using Symbolic Execution to Analyze Linux KBuild Makefiles. International Conference on Software Maintenance and Evolution, New Ideas and Emerging Results (ICSME NIER), pages 712–-716, 2020.
  30. Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, and Armando Solar-Lezama. Program Synthesis with Algebraic Library Specifications. Proc. ACM Program. Lang. (OOPSLA), vol 3, pages 1–25, 2019.
  31. Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic. Programming Language Design and Implementation (PLDI), pages 788–-801. ACM, 2019.
  32. Guolong Zheng, Quang Loc Le, ThanhVu Nguyen, and Quoc-Sang Phan. Automatic data structure repair using separation logic. Java PathFinder Workshop, pages 66–-66, 2018.
  33. Paul Gazzillo, Ugur Koc, Thanhvu Nguyen, and Shiyi Wei. Localizing Configurations in Highly-Configurable Systems. International Systems and Software Product Line Conference, Challenge Track (SPLC), pages 269–-273, 2018.
  34. ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks. A Counterexample-guided Approach to Finding Numerical Invariants. Foundations of Software Engineering (FSE), pages 605–-615. ACM, 2017.
  35. ThanhVu Nguyen, Matthew Dwyer, and William Visser. SymInfer: Inferring Program Invariants using Symbolic States. Automated Software Engineering (ASE), pages 804–-814. IEEE, 2017.
  36. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 301–-318. Springer, 2017.
  37. ThanhVu Nguyen, Ugur Koc, Javran Cheng, Jeffrey S. Foster, and Adam A. Porter. iGen: Dynamic Interaction Inference for Configurable Software. Foundations of Software Engineering (FSE), pages 655–-665. ACM, 2016.
  38. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. Transactions on Software Engineering Methodology (TOSEM), 23(4):30:1–-30:30, 2014.
  39. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Generate Disjunctive Invariants. International Conference on Software Engineering (ICSE), pages 608-–619. IEEE, 2014.
  40. Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, and ThanhVu Nguyen. Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. Automated Reasoning and Mathematics (Essays Memory of William W. McCune), volume 7788, pages 189–-228. Springer, 2013.
  41. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. GenProg: A Generic Method for Automated Software Repair. Transactions on Software Engineering (TSE), 38(1):54–-72, 2012.
    • πŸ…IEEE TSE 50th Anniversary Retrospective Most Influential Paper Award
  42. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Discover Polynomial and Array Invariants. International Conference on Software Engineering (ICSE), pages 683–-693. IEEE, 2012.
    • πŸ…ACM SIGSOFT Distinguished Paper Award
  43. Westley Weimer, Stephanie Forrest, Claire Le Goues, and ThanhVu Nguyen. Automatic Program Repair with Evolutionary Computation. Communications of the ACM (CACM), 53(5):109–-116, 2010.
    • πŸ…Research Highlight
  44. Thang Bui, ThanhVu Nguyen, and Joseph Rizzo. Parallel Shared Memory Strategies For Ant-based Optimization Algorithms. Conference on Genetic and Evolutionary Computation (GECCO), pages 1–8. ACM, 2009.
    • πŸ…Best Paper Award
  45. Stephanie Forrest, Westley Weimer, ThanhVu Nguyen, and Claire Le Goues. A Genetic Programming Approach to Automated Software Repair. Conference on Genetic and Evolutionary Computation (GECCO), pages 947-–954. ACM, 2009.
    • πŸ…Best Paper Award
    • πŸ…ACM SIGEVO 10-year Impact Award
  46. Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie Forrest. Automatically Finding Patches Using Genetic Programming. International Conference on Software Engineering (ICSE), pages 364-–367. IEEE, 2009.
    • πŸ…ACM SIGSOFT Distinguished Paper Award
    • πŸ…Manfred Paul Award for ExcellenceSoftware: Theory and Practice
    • πŸ…ACM SIGSOFT 10-year Most Influential Paper Award
  47. ThanhVu Nguyen, Westley Weimer, Claire Le Goues, and Stephanie Forrest. Using Execution Paths to Evolve Software Patches. International Conference on Software Testing, Verification and Validation Workshops (ICST), pages 152-–153. IEEE, 2009.
    • πŸ…Best Short Paper Award and Best Presentation Award
  48. Thang Bui, ThanhVu Nguyen, Chirag Patel, and Kim-Anh Phan. An Ant-based Algorithm for Coloring Graphs. Discrete Applied Mathematics, 156(2):190-–200, 2008.
  49. James Smith, III and ThanhVu Nguyen. Fuzzy Decision Trees for Planning and Autonomous Control of a Coordinated Team of UAVs. International Society for Optical Engineering. SPIE, May 2007.
  50. James Smith, III and ThanhVu Nguyen. Autonomous and Cooperative Robotic Behavior Based on Fuzzy Logic and Genetic Programming. Integrated Computer-Aided Engineering, 14(2):141-–159, 2007.
  51. James Smith, III and ThanhVu Nguyen. Genetic Program based Data Mining of Fuzzy Decision Trees and Methods of Improving Convergence and Reducing Bloat. International Society for Optical Engineering. SPIE, 2007.
  52. G Viamontes, M Amduka, J Russo, Craven M, and T Nguyen. Efficient Memoization Strategies for Object Recognition with a Multi-Core Architecture. Annual High Performance Embedded Computing Workshop (HPEC). IEEE, 2007.
    • πŸ…Outstanding Submission
  53. Thang Bui and ThanhVu Nguyen. An Agent-based Algorithm for Generalized Graph Colorings. Conference on Genetic and Evolutionary Computation (GECCO), pages 19–-26. ACM, 2006.
    • Erdos number: 4 (through Thang N. Bui)
  54. James Smith, III and ThanhVu Nguyen. Genetic Program based Data Mining to Reverse Engineer Digital Logic. International Society for Optical Engineering, pages 24-–35. SPIE, 2006.
  55. James Smith, III and ThanhVu Nguyen. Resource Manager for an Autonomous Coordinated Team of UAVs. International Society for Optical Engineering, pages 118-–129. SPIE, 2006.
  56. James Smith, III and ThanhVu Nguyen. Creating Fuzzy Decision Algorithms Using Genetic Program Based Data Mining Program. Annual Meeting of the North American Fuzzy Information Processing Society (NAFIPS), pages 471-–477. IEEE, 2006.
  57. James Smith, III and ThanhVu Nguyen. Fuzzy Logic Based Resource Manager for a Team of UAVs. Annual Meeting of the North American Fuzzy Information Processing Society (NAFIPS), pages 463–-470. IEEE, 2006.
  58. James Smith, III and ThanhVu Nguyen. Fuzzy Logic Based UAV Allocation and Coordination. International Conference on Informatics in Control Automation and Robotics (ICINCO), pages 81-–94. Springer, 2006.
    • πŸ…Best Paper Award
  59. James Smith, III and ThanhVu Nguyen. Evolutionary Data Mining Approach to Creating Digital Logic. International Conference on Informatics in Control Automation and Robotics (ICINCO), pages 107-–113. Springer, 2006.
  60. James Smith, III and ThanhVu Nguyen. Guiding Genetic Program Based Data Mining Using Fuzzy Rules. Intelligent Data Engineering and Automated Learning (IDEAL), pages 1337–-1345. Springer, 2006.
  61. James Smith, III and ThanhVu Nguyen. Data Mining based Automated Reverse Engineering and Defect Discovery. International Society for Optical Engineering, pages 232–-242. SPIE, 2005.
  62. James Smith, III and ThanhVu Nguyen. Distributed Autonomous Systems: Resource Management, Planning, and Control Algorithms. International Society for Optical Engineering, pages 65–-76. SPIE, 2005.

Dissertations

  1. Guolong Zheng. Ensure Correctness for Imperative and Declarative Programs. Ph.D. thesis, University of Nebraska-Lincoln, May 2022.
  2. ThanhVu Nguyen. Automating Program Verification and Repair Using Invariant Analysis and Test-input Generation. Ph.D. thesis, University of New Mexico, August 2014.
  3. ThanhVu Nguyen. On the Graph Coloring Problem and Its Generalizations. Master's thesis, The Pennsylvania State University, December 2006.

Acknowledgement

Our work has been generously supported by NSF, Army Research Office, Amazon, Facebook, UNL, and GMU. Thank you!

Contact

George Mason University
Nguyen Engineering Building #4430
4400 University Drive
Fairfax, VA 22030
πŸ“¬  Email: info at roars dot dev