ROARS 🦖 Lab @ GMU

• 9/2025: SSBSE'25 research paper on LLM-guided Input Generation (👏 Didier)
• 9/2025: Two NeurIPS'25 research papers on compositional DNN verification (🏅 NeurIPS Spotlight) and verifying DNN verification (👏 Hai)
• 9/2025:🎁 Received an NVIDIA Academic Research Grant
• 8/2025: ASE'25 research paper on generating challenging benchmarks for DNN verification (👏 Linhan, first research paper as first author)
• 8/2025: NeuralSAT ranked 2nd overall in VNN-COMP'25 (👏 Hai).
• 7/2025: Elevated to ACM Senior Member
• 4/2025: CSConfs: https://roars.dev/csconfs/ is now live. This webapp tracks of upcoming CS conferences
• 4/2025: (Book) Demystifying PhD Admissions in Computer Science is now published and available through Amazon Kindle (the book pdf will always be free through GitHub)
• 4/2025: Two ISSTA'25 tool papers on LSP support for the COOL language (👏 Linhan, first paper) and VS Code support for invariant generation and symbolic execution (👏 Stefania, first paper)
• 4/2025: Elevated to IEEE Senior Member.
• 4/2025: CAV'25 paper on the NeuralSAT DNN verification tool (👏 Hai)
• 2/2025: TSE paper (50th Anniversary Special Issue) on Evolution of APR
• 2/2025: 🏅 TSE 10-Year Retrospective Most Influential Paper Award for GenProg work on automatic program repair (with Claire, Wes, and Steph)
• 1/2025: NeuralSAT ranked 2nd overall in VNN-COMP'24 (our second participation, 👏 Hai). Press: GMU
  Note: An initial parsing issue in the competition scripts undercounted NeuralSAT’s results; the official updated report corrects this and shows NeuralSAT in 2nd place (see Table B.1).
• 1/2025: ICSE'25 NIER paper on LLM-based autoformalization for LEAN (👏 Long, first paper)

• ThanhVu Nguyen (PI, faculty)
• Long Doan (Ph.D. student)
• Hai Duong (Ph.D. student)
• Didier Ishimwe (Ph.D. student)
• Nguyen Ho (Ph.D. student)
• Linhan Li (Ph.D. student)
• Stefania Piciorea (undergraduate)

Lab's

• NeuralSAT ranked 2nd overall in VNN-COMP'25
• Outstanding Teaching Assistants Award 2025 (Linhan@GMU)
• NeuralSAT ranked 2nd overall in VNN-COMP'24
• Outstanding Undergraduate Research Award 2024 (Stefania@GMU)
• NeuralSAT received the New Participant Award at VNN-COMP'23
• Outstanding Undergraduate Senior Award 2023 (KimHao@UNL)
• Outstanding Undergraduate Researcher Award 2021 (KimHao@UNL)

PI's

• IEEE TSE Most Influential Paper Award (50th Anniversary Retrospective) 2025
• Amazon Research Award (Automated Reasoning) 2023
• NSF CAREER Award 2023
• NSF CISE Research Initiation Initiative (CRII) Award 2020
• ACM SIGEVO 10-year Impact Paper Award 2019
• ACM SIGSOFT / IEEE TCSE ICSE 10-year Most Influential Paper Award 2019

• Safe and Robust AI: we are exploring scalable and precise techniques to formally analyze and verify deep neural networks (DNNs).
  • Examples: DPLL(T)-based DNN Verification
• Program Analysis and Invariants Discovery: we have developed dynamic, static, and symbolic techniques to analyze program semantics and to discover and prove interesting properties.
  • Examples: discovering nonlinear polynomial invariants using dynamic analysis (ICSE Distinguished Paper Award); discovering heap-based memory properties using separation logic; generating program interactions in highly-configurable software using decision trees
• Fault Localization and Automated Program Repair: we have developed techniques and tools to automatically identify code region responsible program bugs and modify existing or creating new code to repair the bugs.
  • Examples: C program repair using symbolic testing and genetic programming (10-year ICSE Most Influential Paper Award); localizing faults in model specifications using counterexamples
• LSP-based IDEs: we create extension to bring automated reasoning capabilities to IDEs such as VSCode.

• CSConfs: a webapp to track upcoming CS conferences.
• NeuralSAT: A high-performance deep neural network (DNN) verification tool.
• DIG: A numerical invariant generation tool, focusing on nonlinear polynomials

1. 📚 A book to help students understand 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://roars.dev/phd-cs-us/viet-cs-profs-us: Vietnamese professors in CS

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

1. Didier Ishimwe and ThanhVu Nguyen. LLM-Guided Fuzzing for Pathological Input Generation. Search-Based Software Engineering (SSBSE), 2025
2. Hai Duong, David Shriver, ThanhVu Nguyen, and Matthew Dwyer. Compositional Neural Network Verification via Assume-Guarantee Reasoning. Advances in Neural Information Processing Systems (NeurIPS), 2025
   • 🏅Research Spotlight
3. Hai Duong, ThanhVu Nguyen, and Matthew Dwyer. Generating and Checking DNN Verification Proofs. Advances in Neural Information Processing Systems (NeurIPS), 2025
4. Linhan Li and ThanhVu Nguyen. Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks, Automated Software Engineering (ASE), 2025
5. Stefania Piciorea and ThanhVu Nguyen. Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code. ISSTA-Tool Demo, 2025
6. Linhan Li and ThanhVu Nguyen. COOLer: A Language Support Extension for COOL in VS Code. ISSTA-Tool Demo, 2025
7. Hai Duong, ThanhVu Nguyen, Matthew Dwyer. NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks. Computer Aided Verification (CAV), 2025
8. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. The Evolution of Automated Software Repair. Transactions on Software Engineering (TSE), 2025
9. 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
10. Hai Duong, Dong Xu, ThanhVu Nguyen, Matthew Dwyer. Harnessing Neuron Stability to Improve DNN Verification, Foundations of Software Engineering (FSE), 2024
11. Didier Ishimwe. Inferring Complexity Bounds from Recurrence Relations. Foundations of Software Engineering (Student Research Competition). 2023
12. Tung Dao, Na Meng, and ThanhVu Nguyen. Triggering Modes in Spectrum-Based Multi-Location Fault Localization, Foundations of Software Engineering (FSE) Industry Track, 2023
13. ThanhVu Nguyen and Hai Duong. NeuralSAT: A CDCL-based constraint solving approach to DNN Verification. SIGBED Blog, 2023
14. Quoc-Sang Phan, KimHao Nguyen, ThanhVu Nguyen. Challenges in Shift Left Static Analysis, International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), 2023
15. Guangjing Wang, Nikolay Ivanov, Bocheng Chen, Qi Wang, ThanhVu Nguyen, Qiben Yan, Graph Learning for Interaction Analysis in Smart Home Rule Data, ACM SIGMOD, 2023
16. 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), 2022
17. 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), 2022
18. KimHao Nguyen, ThanhVu Nguyen, and Quoc-Sang Phan. Analyzing the CMake Build System. International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), 2022
19. 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), 2022
20. Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen. Dynaplex: Inferring Asymptotic Runtime Complexity of Recursive Programs. International Conference on Software Engineering- Tool Demo, 2022
21. ThanhVu Nguyen, KimHao Nguyen, and Hai Duong. SymInfer: Inferring Numerical Invariants using Symbolic States. International Conference on Software Engineering-Tool Demo, 2022
22. Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen. Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations, Proc. ACM Program. Lang. (OOPSLA), 2021
23. ThanhVu Nguyen, KimHao Nguyen, Matthew Dwyer. Using Symbolic States to Infer Numerical Invariants, Transactions on Software Engineering (TSE), 2021
24. KimHao Nguyen and ThanhVu Nguyen. GenTree: Using Decision Trees to Learn Interactions for Configurable Software. International Conference on Software Engineering (ICSE), 2021. Artifact Evaluation
25. 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), 2021. Artifact Evaluation
26. 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), 2021. Artifact Evaluation
27. KimHao Nguyen and ThanhVu Nguyen. GenTree: Inferring Configuration Interactions using Decision Trees. Automated Software Engineering (ASE Tool paper), 2021.
28. 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.
29. 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.
30. 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, 2020.
31. 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), 2020.
32. Guolong Zheng, Hamid Bagheri and Thanhvu Nguyen. Debugging Declarative Models in Alloy. International Conference on Software Maintenance and Evolution, Doctoral Symposium (ICSME), 2020.
33. 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), 2020.
34. 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, 2019.
35. 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), ACM, 2019.
36. Guolong Zheng, Quang Loc Le, ThanhVu Nguyen, and Quoc-Sang Phan. Automatic data structure repair using separation logic. Java PathFinder Workshop, 2018.
37. 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), 2018.
38. ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks. A Counterexample-guided Approach to Finding Numerical Invariants. Foundations of Software Engineering (FSE), ACM, 2017.
39. ThanhVu Nguyen, Matthew Dwyer, and William Visser. SymInfer: Inferring Program Invariants using Symbolic States. Automated Software Engineering (ASE), IEEE, 2017.
40. 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), Springer, 2017.
41. 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), ACM, 2016.
42. 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.
43. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Generate Disjunctive Invariants. International Conference on Software Engineering (ICSE), IEEE, 2014.
44. 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, Springer, 2013.
45. 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), 2012.
    • 🏅IEEE TSE 50th Anniversary Retrospective Most Influential Paper Award
46. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Discover Polynomial and Array Invariants. International Conference on Software Engineering (ICSE), IEEE, 2012.
    • 🏅ACM SIGSOFT Distinguished Paper Award
47. Westley Weimer, Stephanie Forrest, Claire Le Goues, and ThanhVu Nguyen. Automatic Program Repair with Evolutionary Computation. Communications of the ACM (CACM), 53(5), 2010.
    
    • 🏅Research Highlight
48. Thang Bui, ThanhVu Nguyen, and Joseph Rizzo. Parallel Shared Memory Strategies For Ant-based Optimization Algorithms. Conference on Genetic and Evolutionary Computation (GECCO), ACM, 2009.
    • 🏅Best Paper Award
49. 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), ACM, 2009.
    • 🏅Best Paper Award
    • 🏅ACM SIGEVO 10-year Impact Award
50. Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie Forrest. Automatically Finding Patches Using Genetic Programming. International Conference on Software Engineering (ICSE), IEEE, 2009.
    • 🏅ACM SIGSOFT Distinguished Paper Award
    • 🏅Manfred Paul Award for ExcellenceSoftware: Theory and Practice
    • 🏅ACM SIGSOFT 10-year Most Influential Paper Award
51. 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), IEEE, 2009.
    • 🏅Best Short Paper Award and Best Presentation Award
52. 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.
53. 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.
54. 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.
55. 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.
56. 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
57. Thang Bui and ThanhVu Nguyen. An Agent-based Algorithm for Generalized Graph Colorings. Conference on Genetic and Evolutionary Computation (GECCO), ACM, 2006.
    • Erdos number: 4 (through Thang N. Bui)
58. James Smith, III and ThanhVu Nguyen. Genetic Program based Data Mining to Reverse Engineer Digital Logic. International Society for Optical Engineering, SPIE, 2006.
59. James Smith, III and ThanhVu Nguyen. Resource Manager for an Autonomous Coordinated Team of UAVs. International Society for Optical Engineering, SPIE, 2006.
60. 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), IEEE, 2006.
61. 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), IEEE, 2006.
62. James Smith, III and ThanhVu Nguyen. Fuzzy Logic Based UAV Allocation and Coordination. International Conference on Informatics in Control Automation and Robotics (ICINCO), Springer, 2006.
    • 🏅Best Paper Award
63. James Smith, III and ThanhVu Nguyen. Evolutionary Data Mining Approach to Creating Digital Logic. International Conference on Informatics in Control Automation and Robotics (ICINCO), Springer, 2006.
64. James Smith, III and ThanhVu Nguyen. Guiding Genetic Program Based Data Mining Using Fuzzy Rules. Intelligent Data Engineering and Automated Learning (IDEAL), Springer, 2006.
65. James Smith, III and ThanhVu Nguyen. Data Mining based Automated Reverse Engineering and Defect Discovery. International Society for Optical Engineering, SPIE, 2005.
66. James Smith, III and ThanhVu Nguyen. Distributed Autonomous Systems: Resource Management, Planning, and Control Algorithms. International Society for Optical Engineering, SPIE, 2005.

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.