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
1/2026: BibTeX Parser: https://roars.dev/bibtex/ is now live. This webapp displays publications from a BibTeX file.
1/2026: FSE'26 research paper on formalizing and verifying structural robustness properties of AI systems (π Hai)
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)
4/2024: Nguyen and Long joined as PhD students
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
12/2022: ICSE SEIP paper on shift left static analysis (π KimHao)
11/2022: π Thanksgiving party!!!
11/2022: SIGMOD'23 research paper on using graph neural networks to analyze IoT interactive bugs
8/2022: π Start of the semester party!!!
8/2022: Hai joined as a Ph.D. student
7/2022: ASE'22 research paper on feed-back driven iterative Alloy repair (π Guolong)
4/2022: π Guolong defended his dissertation on Alloy analysis (first Ph.D. alumni of the group!)
4/2022: ISSTA'22 research paper on template-based Alloy repair (π Guolong)
/12022: TwoICSE Tool papers on complex analysis (π Didier) and invariant generation (π KimHao and Hai)
1/2022: ICSE SEIP paper on analyzing CMake build scripts (π KimHao)
1/2022: Linhan joined as a Ph.D. student
12/2021: ICSE NIER paper on Graph Neural Networks analysis
9/2021: OOPSLA'21 research paper on capturing runtime complexity of recursive programs (π Didier and KimHao)
9/2021: TSE'21 journal paper on symbolic states and dynamic invariant inference (π KimHao)
8/2021: π Received a gift from Meta/Facebook to work on build systems and symbolic execution
8/2021: π Received an NSF Collaborative (Medium) Grant to dynamically analyze program liveness and safety properties
8/2021: π Farewell party!!!
7/2021: ThreeASE Tool papers (π KimHao and Guolong)
6/2021: π Moving to George Mason University (Fall'21)
5/2021: π Outstanding Undergraduate Research Assistant Award from UNL CSE (π KimHao)
5/2021: π Alexey defended his Master's thesis
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
1/2020: Alexey joined as an M.S. student
9/2019: OOPSLA'19 research paper on using algebraic specifications to aid program synthesis
9/2019: Didier joined as a Ph.D. student
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
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)
PI's
IEEE TSE Most Influential Paper Award (50th Anniversary Retrospective) 2025
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 deep neural network (DNN) verification tool.
DIG: A numerical invariant generation tool, focusing on nonlinear polynomials
CSPicks: a webapp to explore CS faculty and PhD programs.
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
Teaching
Previous
Software Specification and Construction: SWE 419/619
(student feedback)
