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

DynaROARS πŸ¦– Lab @ GMU

AI-generated DinoROARS Mascot

Welcome to DynaROARS (DYNAmic, RigOrous, and Automated Reasoning Systems) Lab at George Mason University.

News

Older News

People

Lab activities/photos

Alumni

πŸ₯· Student Recruitment

Interested in our research in safe and robust AI and software analysis? Read how to demystify the CS PhD admission process in the US and why you would want to join CS@GMU.

Interested?
  • Read "Should you contact a US professor? How to do so correctly?" from the CS PhD Admission Demystify Handbook.
  • Email us the following:
    • Why are you interested in working with us? Be as specific as possible, e.g., you have read our papers or if you have worked on something related, discuss them. we will not read or reply to your email if it is generic (i.e., could be sent to multiple professors)
    • Try the following programming assignments PA1 and PA2. Email all solutions in a zip file. This gives you a sense on what background you would need and allows us to evaluate your skills.
    • Put "Dynaroars Lab Applicant" in the subject line of the email
    • Do not attach your transcripts, GRE, or any other standard scores
    • Send your email using plain text (no colors or fancy fonts)
  • Note that we might not be able to respond to all mails received, especially those that might not fit our lab. However, we still encourage you to apply to GMU and feel free to put us in your SOP.
  • Preferred qualifications: mathematical background and programming skills. We are especially interested in those with experience in programming competitions, e.g., won prize in national or international math/programming contests.

Recent 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

Publications

Google Scholars for Dynaroars

Blog: various posts from Dynaroars' members

Unpublished/Under Submission

  1. Hai Duong, ThanhVu Nguyen, Matthew Dwyer, A DPLL(T) Framework for Verifying Deep Neural Networks, Arxiv, 2023
  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, 2023
  3. Linhan Li and ThanhVu Nguyen, COOLIO: A Language Support Extension for the Classroom Object Oriented Language, Arxiv, 2023.

Published/To-appear Papers

  1. Hai Duong, Dong Xu, ThanhVu Nguyen, Matthew Dwyer. Harnessing Neuron Stability to Improve DNN Verification, Foundations of Software Engineering (FSE). 20 pages (to appear), 2024
  2. Didier Ishimwe. Inferring Complexity Bounds from Recurrence Relations. Foundations of Software Engineering (Student Research Competition). 2023
  3. 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
  4. ThanhVu Nguyen and Hai Duong. NeuralSAT: A CDCL-based constraint solving approach to DNN Verification. SIGBED Blog, 2023
  5. KimHao Nguyen, ThanhVu Nguyen, and Quoc-Sang Phan. Challenges in Shift Left Static Analysis, International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), 340--342, 2023
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. ThanhVu Nguyen, KimHao Nguyen, Matthew Dwyer. Using Symbolic States to Infer Numerical Invariants, Transactions on Software Engineering (TSE), 2021
  15. 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
  16. 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
  17. 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
  18. KimHao Nguyen and ThanhVu Nguyen. GenTree: Inferring Configuration Interactions using Decision Trees. Automated Software Engineering (ASE Tool paper), 2021.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. ThanhVu Nguyen, Matthew Dwyer, and William Visser. SymInfer: Inferring Program Invariants using Symbolic States. Automated Software Engineering (ASE), pages 804–-814. IEEE, 2017.
  31. 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.
  32. 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.
  33. 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.
  34. 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.
  35. 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.
  36. 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.
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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.
  44. 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.
  45. 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.
  46. 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.
  47. 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
  48. 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)
  49. 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.
  50. 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.
  51. 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.
  52. 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.
  53. 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
  54. 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.
  55. 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.
  56. 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.
  57. 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.

Miscs

  1. πŸ““ A handbook to help students demystify 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

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: tvn at gmu dot edu