Welcome to ROARS (Research on Automated Reasoning Systems) Lab at George Mason University.
We develop automated reasoning techniques to formalize, verify, and analyze software and AI systems. See Research for more information.
News
5/2026: ICML'26 research paper on (invariant) generation of randomized self-reductions for mathematical functions received ICML Spotlight
5/2026: Hai received the Oustanding PhD Student Award from GMU CS and is interning at Amazon AWS in the summer
4/2026: CVPR'26 research paper on verifying AI-based computer vision systems received CVPR Highlight (π Hai)
4/2026: Serving as an organizer and program (papers) chair of VNN-COMP'26, the annual competition on verifying neural networks. Consider submitting your NNV tools and related papers
4/2026: π Didier defended his dissertation on complexity analysis (second PhD alumni of the group!). Plenty of pictures from the defense from the lab photos.
4/2026: Amazon Research Award (2nd ARA Award) for Verifiable AI and ML-assisted Mathematical Reasoning
3/2026: π Ongoing work on an introductory textbook for neural network verification
3/2026: TSE'26 research paper on specification repair and test generation
2/2026: CS GMU People: a webapp listing faculty and staff at CS GMU.
4/2025: Serving as an organizer and program (papers) chair of VNN-COMP'25, the annual competition on verifying neural networks. Consider submitting your NNV tools and related papers.
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: TwoISSTA'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). GMU News
1/2025: NeuralSATranked 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 (Table B.1).
1/2025: ICSE'25 NIER paper on LLM-based autoformalization for LEAN (π Long, first paper)
11/2024: π Thanksgiving party!!!
8/2024: Appointed Director of the MS Software Engr program
8/2024: Promoted to Associate Professor with tenure
6/2024: π Received an NSF Collaborative Formal Methods in the Field (FMitF) Grant
5/2024: π Outstanding Undergraduate Research Award from GMU (π Stefania)
3/2024: Stefania joined as a undergraduate researcher
2/2024: FSE'24 research paper on new optimizations developed for the NeuralSAT DNN verification tool (π Hai, first research paper as first author)
1/2024: NeuralSAT ranked 4th overall and received the New Participant Award at VNN-COMP'23 (our first participation). It also won the tllverifybench category (π Hai and Linhan)
1/2024: Huong joined as a undergraduate researcher
11/2023: π Thanksgiving party!!!
8/2023: NeuralSATranked 4th overall in the annual Verifying Neural Network competition VNN-COMP'23 (our first participation, π Hai and Linhan)
8/2023: FSE SRC (Student Research Competition) paper on dynamic complexity analysis (π Didier)
8/2023: FSE'23 Industry paper on fault localization
7/2023: π Received an NSF Formal Methods in the Field (FMitF) Grant
4/2021: π KimHao received the Top Presentation Award on analyzing configurable systems at the Nebraska Student Research Days
12/2020: Three research papers accepted at ICSE'21 on inferring interactions in
configurable software and debugging and repairing Alloy specifications (π KimHao and Guolong)
12/2020: π Received a Faculty Seed Grant Award from UNL
10/2020: OOPSLA'20 research paper on using dynamically inferred nonlinear invariants to prove program termination and non-termination
9/2020: π UCare Award from UNL and the Garmin Scholarship Award (π KimHao)
8/2020: FSE SEAD workshop paper on using recurrence relations to analyze program complexity (π Alexey and Didier)
7/2020: ICSME NIER paper on using symbolic execution to analyze the Linux build system (π KimHao)
7/2020: ICSME Doctoral Symposium paper on Alloy fault
localization and repair (π Guolong)
3/2020: π Received the NSF CISE Research Initiation Initiative (CRII) Award on analyzing the Linux build system.
Press: UNL
3/2020: KimHao (freshman) joined as an undergraduate researcher
6/2019: π π Received an ACM SIGSOFT 10-year Most Influential Paper Award at ICSE
(Software Engr) on program repair. Also an ACM SIGEVO 10-year Impact Award
at GECCO (Evolutionary Computing) on using genetic programming to fix
bugs
3/2019: PLDI'19 research paper on dynamic invariant inference in separation logic (π Guolong)
1/2019: π Received a 3-year grant from the Army Research Office to work on program errors prediction and avoidance
Contribute to our open-source projects, e.g., an easy one to work on is csconfs---a webapp to track CS conferences. You can creating Github issues and pull requests for the project. This shows you're serious about working with us and allows us to evaluate your skills.
Note: Unless there is a strong match and interest, we will not be able to respond to your emails, especially if they are generic.
Awards
Lab's
Research Spotlight at ICML'26
Outstanding CS PhD Student Award 2026 (Hai@GMU)
Research Highlight at CVPR'26
Best Paper Award at SSBSE'25
Research Spotlight at NeurIPS'25
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)
UNL press release on ACM SIGSOFT 10-year Most Influential Paper Award at ICSE
Research
Software Engineering; Formal Methods; Automated Reasoning; Program Analysis; Program Verification; AI Safety and Robustness, Dynamic and Static Analysis; SMT/SAT Solving
Safe and Robust AI: we are exploring scalable and precise techniques
to formally analyze and verify deep neural networks (DNNs).
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
NeuralSAT: A high-performance neural network verification tool.
DIG: A numerical invariant generation tool, focusing on nonlinear polynomials.
CSPicks: a webapp to explore CS faculty and PhD programs.
CS GMU People: a webapp for CS GMU directory (faculty and staff).
BibTex Parser: a webapp to display publications from a BibTeX file.
CSConfs: a webapp to track upcoming CS conferences.
More
NLA-Digbench: this
SV-COMP benchmark contains various program with nonlinear invariants and properties.
Solving NP-Complete problems
AntColor: an ant-based heuristics for the graph coloring problem and its generalizations
AMC: a fast, parallel ant-based algorithm for the maximum clique problem
NP Benchmarks: a comprehensive collection of benchmarks (in DIMACS format) for various NP-Complete problems including graph coloring, maximum clique, vertex cover, and spanning tree
