example.bib

@preamble{ "\newcommand{\tseif}{9.3}" }
@preamble{ "\newcommand{\cacmif}{14.07}" }
@preamble{ "\newcommand{\pacmpl}{14.07}" }

@string{neurips = {Advances in Neural Information Processing Systems (NeurIPS)}}
@string{ase = {Automated Software Engineering (ASE)}}

@string{cav = {Computer Aided Verification (CAV)}}

@string{issta = {International Symposium on Software Testing and Analysis (ISSTA)}}

@string{cacm = {Communications of the ACM (CACM)}}

@string{fse = {Foundations of Software Engineering (FSE)}}

@string{gecco = {Conference on Genetic and Evolutionary Computation (GECCO)}}

@string{icse = {International Conference on Software Engineering (ICSE)}}

@string{oopsla = {(OOPSLA)}}

@string{pldi = {Programming Language Design and Implementation (PLDI)}}

@string{tacas = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}}

@string{sigmod = {International Conference on Management of Data (SIGMOD)}}

@string{tosem = {Transactions on Software Engineering Methodology (TOSEM)}}

@string{tse = {Transactions on Software Engineering (TSE)}}

@string{spie = {Society of Photo-Optical Instrumentation Engineers (SPIE)}}



@article{duong2026verifyingc,
    author={Duong$^3$, Hai and Le, Thanh and Lam, Nguyen and Nguyen, ThanhVu},
	note = {\href{https://roars.dev/pubs/na.pdf}{PDF}},
    crossref={duong2026verifying}
}


@article{duong2026verifying,
    author={Duong, Hai and Le, Thanh and Lam, Nguyen and Nguyen, ThanhVu},
    title={{Harnessing Neuron Stability to Improve DNN Verification}},
    journal = {Proceedings of the ACM on Software Engineering (PACMSE)},
    volume={},
    number={FSE},
    year={2026},
    pages={to appear}
}

@misc{kaulen20256thinternationalverificationneural,
      title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, 
      author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu},
      year={2025},
      eprint={2512.19007},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2512.19007}, 
}

@inproceedings{ishimwe2025llmc,
  author={Ishimwe, Didier$^3$ and Nguyen, ThanhVu},
  crossref={ishimwe2025llm},
  note = {\href{https://roars.dev/pubs/na.pdf}{PDF}},
  note_award = {Best Paper Award}
}

@inproceedings{ishimwe2025llm,
  title     = {LLM-Guided Fuzzing for Pathological Input Generation},
  author    = {Ishimwe, Didier and Nguyen, ThanhVu},
  booktitle = {International Symposium on Search Based Software Engineering},
  pages     = {to appear},
  year      = {2025},
  organization={Springer}
}


@inproceedings{duong2025compositionalc,
  author={Duong$^3$, Hai and Shriver, David and Nguyen, ThanhVu and Dwyer, Matthew},
  crossref={duong2025compositional},
  note = {\href{https://roars.dev/pubs/duong2025compositional.pdf}{PDF}},
  note_award = {Research Spotlight}
}

@inproceedings{duong2025compositional,
  title     = {Compositional Neural Network Verification via Assume-Guarantee Reasoning},
  author    = {Duong, Hai and Shriver, David and Nguyen, ThanhVu and Dwyer, Matthew},
  booktitle = neurips,
  volume    = {},
  pages     = {to appear},
  year      = {2025},
  editor    = {}
}



@inproceedings{duong2025generatingc,
  author={Duong$^3$, Hai and Nguyen, ThanhVu and Dwyer, Matthew},
  crossref={duong2025generating},
  note = {\href{https://roars.dev/pubs/duong2025generating.pdf}{PDF}}
}


@inproceedings{duong2025generating,
  title     = {Generating and Checking DNN Verification Proofs},
  author    = {Duong, Hai and Nguyen, ThanhVu and Dwyer, Matthew},
  booktitle = neurips,
  volume    = {},
  pages     = {to appear},
  year      = {2025},
  editor    = {}
}

@inproceedings{duong2025neuralsat2c,
  author={Duong$^3$, Hai and Nguyen, ThanhVu},
  crossref={duong2025neuralsat2},
  note = {\href{https://roars.dev/pubs/na.pdf}{PDF}}
}

@inproceedings{duong2025neuralsat2,
  title={Neuralsat: Scaling constraint solving for dnn verification (competition contribution)},
  author={Duong, Hai and Nguyen, ThanhVu},
  booktitle={International Symposium on AI Verification},
  pages={253--259},
  year={2025},
  organization={Springer}
}


@inproceedings{li2025destabilizingc,
	author = {Li$^3$, Linhan and Nguyen, ThanhVu},
	booktitle = ASE,
	crossref = {li2025destabilizing},
	note = {\href{https://roars.dev/pubs/li2025destabilizing.pdf}{PDF}}}
@inproceedings{li2025destabilizing,
	author = {Li, Linhan and Nguyen, Thanhvu},
	booktitle = ASE,
	pages = {to appear},
	publisher = {IEEE},
	title = {Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks},
	year = {2025}}

@inproceedings{li2025coolerc,
    author = {Li$^3$, Linhan and Nguyen, ThanhVu},
    note = {\href{https://roars.dev/pubs/li2025cooler.pdf}{PDF}},
    crossref={li2025cooler}
}
@inproceedings{li2025cooler,
	author = {Li, Linhan and Nguyen, ThanhVu},
	booktitle = ISSTA # "-Tool Demo",
	title = {{COOLer: A Language Support Extension for COOL in VS Code}},
    publisher = {ACM},
    pages={11--15},
	year = {2025}
}

@inproceedings{piciorea2025bringingc,
    author = {Piciorea$^1$, Stefania and Nguyen, ThanhVu},
    note = {\href{https://roars.dev/pubs/piciorea2025bringing.pdf}{PDF}},
    crossref={piciorea2025bringing}
}
@inproceedings{piciorea2025bringing,
	author = {Piciorea, Stefania and Nguyen, ThanhVu},
	booktitle = ISSTA # "-Tool Demo",
	title = {{Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code}},
    publisher = {ACM},
    pages={51--55},
	year = {2025}
}


@inproceedings{duong2025neuralsatc,
	author = {Duong$^3$, Hai and Nguyen, ThanhVu and Dwyer, Matthew},
    note = {\href{https://roars.dev/pubs/duong2025neuralsat.pdf}{PDF}},
    crossref={duong2025neuralsat}
}
@inproceedings{duong2025neuralsat,
	author = {Duong, Hai and Nguyen, ThanhVu and Dwyer, Matthew},
	booktitle = CAV,
    pages = {409--423},
	title = {NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks},
	year = {2025}}

@article{le2025evolutionc,
crossref={le2025evolution},
note = {\href{https://roars.dev/pubs/le2025evolution.pdf}{PDF}}
}

@article{le2025evolution,
  title={The Evolution of Automated Software Repair},
  author={Le Goues, Claire and Nguyen, ThanhVu and Forrest, Stephanie and Weimer, Westley},
  journal={IEEE Transactions on Software Engineering},
  year={2025},
  publisher={IEEE}
}


@inproceedings{doan2025aic,
    author={Doan$^3$, Long and Nguyen, ThanhVu H},
    note = {\href{https://roars.dev/pubs/doan2025ai.pdf}{PDF}},
    crossref={doan2025ai}
}

@inproceedings{doan2025ai,
  title={AI-Assisted Autoformalization of Combinatorics Problems in Proof Assistants},
  author={Doan, Long and Nguyen, ThanhVu H},
  booktitle = ICSE # "-New Ideas and Emerging Results (ICSE-NIER)", 
  pages={1--5},
  year={2025}
}

@article{duong2024harnessingc,
    author={Duong$^3$, Hai  and Xu, Dong and Nguyen, ThanhVu and Dwyer, Matthew},
	note = {\href{https://roars.dev/pubs/duong2024harnessing.pdf}{PDF}},
    crossref={duong2024harnessing}
}


@article{duong2024harnessing,
    author={Duong, Hai  and Xu, Dong and Nguyen, ThanhVu and Dwyer, Matthew},
    title={{Harnessing Neuron Stability to Improve DNN Verification}},
    journal = {Proceedings of the ACM on Software Engineering (PACMSE)},
    volume={1},
    number={FSE},
    year={2024},
    pages={859--881}
}

@inproceedings{dao2023triggeringc,
crossref={dao2023triggering}
}
@inproceedings{dao2023triggering,
	author = {Dao, Tung and Meng, Na and Nguyen, ThanhVu},
	booktitle = FSE # "-Industry Track", 
	pages={1774--1785},
	title = {Triggering Modes in Spectrum-Based Multi-Location Fault Localization},
	year = {2023}}



@misc{liu2023drnlac,
crossref={liu2023drnla}
}
@misc{liu2023drnla,
      title={DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing}, 
      author={Yuandong Cyrus Liu and Ton-Chanh Le and Timos Antonopoulos and Eric Koskinen and ThanhVu Nguyen},
      year={2023},
      note={journal, 30 pages},
      eprint={2306.15584},
      archivePrefix={arXiv},
      primaryClass={cs.PL}
}

@misc{duong2023dplltc,
crossref={duong2023dpllt},
author={Hai Duong$^3$ and Linhan Li$^3$ and ThanhVu Nguyen and Matthew Dwyer},
}

@misc{duong2023dpllt,
      title={A DPLL(T) Framework for Verifying Deep Neural Networks}, 
      author={Hai Duong and Linhan Li and ThanhVu Nguyen and Matthew Dwyer},
      year={2023},
      note={journal, 25 pages},
      eprint={2307.10266},
      archivePrefix={arXiv},
      primaryClass={cs.LG}
}

@article{wang2023graphc,
	crossref = {wang2023graph},
	note = {\href{https://roars.dev/pubs/wang2023graph.pdf}{PDF}}
}

@article{wang2023graph,
  title={{Graph Learning for Interaction Analysis in Smart Home Rule Data}},
  author={Wang, Guangjing and  Ivanov, Nikolay and  Chen, Bocheng and Wang, Qi and Nguyen, ThanhVu and Yan, Qiben},
  journal={Proceedings of the ACM on Management of Data (SIGMOD)},
  pages={1--27},
  year={2023},
  publisher={ACM}
}


@inproceedings{phan2023challengesc,
	crossref = {phan2023challenges},
        author={Phan, Quoc-Sang and Nguyen$^1$, KimHao and Nguyen, ThanhVu},
	note = {\href{https://roars.dev/pubs/phan2023challenges.pdf}{PDF}}
    }


@inproceedings{phan2023challenges,
  title={The Challenges of Shift Left Static Analysis},
  author={Phan, Quoc-Sang and Nguyen, KimHao and Nguyen, ThanhVu},
  booktitle = ICSE # "-Software Engineering in Practice (ICSE-SEIP)",   
  pages={340--342},
  year={2023},
  publisher={IEEE}
}




@inproceedings{nguyen2022towardc,
	addendum = {Acceptance 28\%\coe{, contribution 75\%}},
	crossref = {nguyen2022toward},
	note = {\href{https://roars.dev/pubs/nguyen2022toward.pdf}{PDF}}}

@inproceedings{nguyen2022toward,
  title={Toward the Analysis of Graph Neural Networks},
  author={Nguyen, Thanh-Dat and Le-Cong, Thanh and Nguyen, ThanhVu H and Le, Xuan-Bach D and Huynh, Quyet-Thang},
  booktitle= icse # "-New Ideas and Emerging Results (NIER)",
  pages={116--120},
  year={2022}
}



@inproceedings{nguyen2022syminferc,
	addendum = {Acceptance 50\%\coe{, contribution 75\%}},
	author = {Nguyen, ThanhVu and Nguyen$^1$, KimHao and Duong$^3$, Hai},
	crossref = {nguyen2022syminfer},
	note = {\href{https://roars.dev/pubs/nguyen2022syminfer.pdf}{PDF}}}

@inproceedings{nguyen2022syminfer,
  title={SymInfer: Inferring Numerical Invariants using Symbolic States},
  author={Nguyen, ThanhVu and Nguyen, KimHao and Duong, Hai},
  booktitle = ICSE # "-Tool Demo", 
  pages={197--201},
  year={2022},
  publisher={IEEE}
}

@article{ishimwe2023recurc,
	author = {Ishimwe, Didier$^3$ and Nguyen, ThanhVu},
	crossref = {ishimwe2023recur}
        }

@article{ishimwe2023recur,
	author = {Ishimwe, Didier and Nguyen, ThanhVu},
	journal = {Proceedings of the ACM on Programming Languages},
	number = {OOPSLA},
	pages = {under submission},
	publisher = {ACM},
	title = {{RECUR: Inferring and Solving Recurrences to Analyze Program  Complexity}},
	volume = {},
	year = {2023}}

@inproceedings{ishimwe2022dynaplexc,
	addendum = {Acceptance 50\%\coe{, contribution 33\%}},
	author = {Ishimwe$^3$, Didier and Nguyen$^1$, KimHao and Nguyen, ThanhVu},
	crossref = {ishimwe2022dynaplex},
	note = {\href{https://roars.dev/pubs/ishimwe2022dynaplex.pdf}{PDF}}}
@inproceedings{ishimwe2022dynaplex,
  title={Dynaplex: Inferring Asymptotic Runtime Complexity of Recursive Programs},
  author={Ishimwe, Didier and Nguyen, ThanhVu and Nguyen, KimHao},
  booktitle = ICSE # "-Tool Demo", 
  pages={61--64},
  year={2022},
  publisher={IEEE}
}




@article{ishimwe2021dynaplexc,
	author = {Ishimwe$^3$, Didier and Nguyen$^1$, KimHao and Nguyen, ThanhVu},
	crossref = {ishimwe2021dynaplex},
	note = {\href{https://roars.dev/pubs/ishimwe2021dynaplex.pdf}{PDF}},
	number = OOPSLA}

@article{ishimwe2021dynaplex,
	author = {Ishimwe, Didier and Nguyen, KimHao and Nguyen, ThanhVu},
	journal = {Proceedings of the ACM on Programming Languages},
	number = {OOPSLA},
	pages = {1--23},
	publisher = {ACM},
	title = {{Dynaplex: analyzing program complexity using dynamically inferred recurrence relations}},
	volume = {5},
	year = {2021}}

@article{nguyen2021usingc,
	addendum = {Impact Factor \tseif{}},
	author = {Nguyen, Thanhvu and Nguyen$^1$, KimHao and Dwyer, Matthew},
	crossref = {nguyen2021using},
	journal = TSE,
	note = {\href{https://roars.dev/pubs/nguyen2021using.pdf}{PDF}}}

@article{nguyen2021using,
	author = {Nguyen, Thanhvu and Nguyen, KimHao and Dwyer, Matthew},
	journal = {Transactions on Software Engineering},
	publisher = {IEEE},
	title = {Using Symbolic States to Infer Numerical Invariants},
        volume={48},
        number={10},
        pages={3877-–3899},
	year = {2021}}



@inproceedings{nguyen2021gentreec,
	addendum = {Acceptance 22\%, \href{https://roars.dev/pubs/nguyen2021artifact.pdf}{artifact evaluation}},
	author = {Nguyen$^1$, KimHao and Nguyen, ThanhVu},
	booktitle = ICSE,
	crossref = {nguyen2021gentree},
	note = {\href{https://roars.dev/pubs/nguyen2021gentree.pdf}{PDF}}}

@inproceedings{nguyen2021gentree,
	author = {Nguyen, KimHao and Nguyen, ThanhVu},
	booktitle = ICSE,
	publisher = {IEEE},
	pages = {1598--1609},
	title = {GenTree: Using decision trees to learn interactions for configurable software},
	year = {2021}}


@inproceedings{zheng2021toolc,
	addendum = {Acceptance 47\%},
	author = {Zheng$^3$, Guolong and Nguyen, ThanhVu and Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Frias, Marcelo F and Aguirre, Nazareno and Bagheri, Hamid},
	crossref = {zheng2021tool},
	note = {\href{https://roars.dev/pubs/zheng2021tool.pdf}{PDF}}}


@inproceedings{nguyen2021toolc,
	addendum = {Acceptance 47\%},
	author = {Nguyen$^1$, KimHao and Nguyen, ThanhVu},
	crossref = {nguyen2021tool},
	note = {\href{https://roars.dev/pubs/nguyen2021tool.pdf}{PDF}}}

@inproceedings{nguyen2021tool,
	author = {Nguyen, KimHao and Nguyen, ThanhVu},
	booktitle = ASE # "-Tool Demo", 
	title = {GenTree: Inferring Configuration Interactions using Decision Trees},
        publisher = {IEEE},
        pages={1232--1236},
	year = {2021}}



@inproceedings{nguyen2017syminferc,
	addendum = {Acceptance 21\%},
	booktitle = ASE,
	crossref = {nguyen2017syminfer},
	note = {\href{https://roars.dev/pubs/nguyen2017syminfer.pdf}{PDF}}}
@inproceedings{nguyen2017syminfer,
	author = {Nguyen, ThanhVu and Dwyer, Matthew and Visser, William},
	booktitle = ASE,
	pages = {804--814},
	publisher = {IEEE},
	title = {SymInfer: Inferring Program Invariants using Symbolic States},
	year = {2017}}



@inproceedings{brida2022icebarc,
	addendum = {Acceptance 22\%\coe{, contribution 14\%}},
author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng$^3$, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
        booktitle = ASE,        
	crossref = {brida2022icebar},      
	note = {\href{https://roars.dev/pubs/brida2022icebar.pdf}{PDF}}}

@inproceedings{brida2022icebar,
  author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
  booktitle = ASE,
  title = {ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications},
  year = 2022,
  pages={1--13},
  publisher = {ACM}
        }


@inproceedings{zheng2022atrc,
	addendum = {Acceptance 26.6\%\coe{, contribution 14\%}},
  author={Zheng$^3$, Guolong and Nguyen, ThanhVu and Gutiérrez Brida, Simón and Regis, Germán and Frias, Marcelo and Aguirre, Nazareno and Bagheri, Hamid},
  booktitle= ISSTA,
	crossref = {zheng2022atr},
	note = {\href{https://roars.dev/pubs/zheng2022atr.pdf}{PDF}}}

@inproceedings{zheng2022atr,
  author={Zheng, Guolong and Nguyen, ThanhVu and Gutiérrez Brida, Simón and Regis, Germán and Frias, Marcelo and Aguirre, Nazareno and Bagheri, Hamid},
  booktitle={ISSTA},
  title={{ATR: Template-based Repair for Alloy Specifications}},
  year={2022},
  pages={666--677},
  publisher = {ACM}
}



@inproceedings{nguyen2022analyzingc,
	crossref = {nguyen2022analyzing},
        author={Nguyen$^1$, KimHao and Nguyen, ThanhVu and Phan, Quoc-Sang},
	note = {\href{https://roars.dev/pubs/nguyen2022analyzing.pdf}{PDF}}}

@inproceedings{nguyen2022analyzing,
  title={Analyzing the CMake Build System},
  author={Nguyen, KimHao and Nguyen, ThanhVu and Phan, Quoc-Sang},
  booktitle = ICSE # "-Software Engineering in Practice (ICSE-SEIP)",     
  pages={27--28},
  year={2022},
  publisher={IEEE}
}

@inproceedings{nguyen2021artifact,
	author = {Nguyen, KimHao and Nguyen, ThanhVu},
    booktitle = ICSE # "-Companion Proceedings (ICSE-Companion)",       
	publisher = {IEEE},
	pages = {177--178},
	title = {Artifact for" GenTree: Using Decision Trees to Learn Interactions for Configurable Software"},
	year = {2021}}


@inproceedings{zheng2021tool,
	author = {Zheng, Guolong and Nguyen, ThanhVu and Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Frias, Marcelo F and Aguirre, Nazareno and Bagheri, Hamid},
	booktitle = ASE # "-Tool Demo", 
    publisher = {IEEE},
    pages={1218--1222},
	title = {FLACK: Localizing Faults in Alloy Models},
	year = {2021}}

@inproceedings{zheng2021artifact,
	author = {Zheng, Guolong and Nguyen, ThanhVu and Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Frias, Marcelo F and Aguirre, Nazareno and Bagheri, Hamid},
    booktitle = ICSE # "-Companion Proceedings (ICSE-Companion)",           
	publisher = {IEEE},
	pages = {179--180},
	title = {Artifact of `FLACK: Counterexample-Guided Fault Localization for Alloy Models'},
	year = {2021}}

@inproceedings{zheng2021flackc,
	addendum = {Acceptance 22\%, \href{https://roars.dev/pubs/zheng2021artifact.pdf}{artifact evaluation}},
	author = {Zheng$^3$, Guolong and Nguyen, ThanhVu and Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Frias, Marcelo F and Aguirre, Nazareno and Bagheri, Hamid},
	booktitle = ICSE,
	crossref = {zheng2021flack},
	note = {\href{https://roars.dev/pubs/zheng2021flack.pdf}{PDF}}}

@inproceedings{zheng2021flack,
	author = {Zheng, Guolong and Nguyen, ThanhVu and Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Frias, Marcelo F and Aguirre, Nazareno and Bagheri, Hamid},
	booktitle = ICSE,
	publisher = {IEEE},
	pages = {637--648},
	title = {FLACK: Counterexample-guided fault localization for alloy models},
	year = {2021}}

@inproceedings{brida2021toolc,
	addendum = {Acceptance 47\%},
	author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng$^3$, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
	crossref = {brida2021tool},
	note = {\href{https://roars.dev/pubs/brida2021tool.pdf}{PDF}}}

@inproceedings{brida2021tool,
	author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
	booktitle = ASE # "-Tool Demo", 
	  pages={1213--1217},
	title = {BeAFix: An Automated Repair Tool for Faulty Alloy Models},
        publisher = {IEEE},
	year = {2021}}

@inproceedings{brida2021boundedc,
	addendum = {Acceptance 22\%, \href{https://roars.dev/pubs/brida2021artifact.pdf}{artifact evaluation}},
	author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng$^3$, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
	booktitle = ICSE,
	crossref = {brida2021bounded},
	note = {\href{https://roars.dev/pubs/brida2021bounded.pdf}{PDF}}}

@inproceedings{brida2021bounded,
	author = {Brida, Sim{\'o}n Gutierrez and Regis, Germ{\'a}n and Zheng, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
	booktitle = {International Conference on Software Engineering (ICSE)},
	publisher = {IEEE},
	pages = {1135--1147},
	title = {Bounded exhaustive search of alloy specification repairs},
	year = {2021}}

@inproceedings{brida2021artifact,
	author = {Brida, Sim{\'o}n Guti{\'e}rrez and Regis, Germ{\'a}n and Zheng, Guolong and Bagheri, Hamid and Nguyen, ThanhVu and Aguirre, Nazareno and Frias, Marcelo},
	booktitle = {International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)},
	publisher = {IEEE},
	pages = {209--210},
	title = {Artifact of Bounded Exhaustive Search of Alloy Specification Repairs},
	year = {2021}}

@article{le2020dynamitec,
	crossref = {le2020dynamite},
	note = {\href{https://roars.dev/pubs/le2020dynamite.pdf}{PDF}},
	number = OOPSLA}

@article{le2020dynamite,
	author = {Le, TonChanh and Antonopoulos, Timos and Fathololumi, Parisa and Koskinen, Eric and Nguyen, ThanhVu},
	journal = {Proceedings of the ACM on Programming Languages},
	number = {OOPSLA},
	pages = {1--30},
	publisher = {ACM New York, NY, USA},
	title = {DynamiTe: Dynamic Termination and Non-termination Proofs},
	volume = {4},
	year = {2020}}

@inproceedings{nguyen2020using2c,
	addendum = {Acceptance 37\%},
	author = {Nguyen, ThanhVu and Nguyen$^1$, KimHao},
	crossref = {nguyen2020using2},
	note = {\href{https://roars.dev/pubs/nguyen2020using2.pdf}{PDF}}}

@inproceedings{nguyen2020using2,
	author = {Nguyen, ThanhVu and Nguyen, KimHao},
	booktitle = {International Conference on Software Maintenance and Evolution},
	publisher = {IEEE},
	pages = {712--716},
	title = {Using Symbolic Execution to Analyze Linux KBuild Makefiles},
	year = {2020}}

@inproceedings{zheng2020debuggingc,
	author = {Zheng$^3$, Guolong and Bagheri, Hamid and Nguyen, ThanhVu},
	crossref = {zheng2020debugging},
	note = {\href{https://roars.dev/pubs/zheng2020debugging.pdf}{PDF}}}

@inproceedings{zheng2020debugging,
	author = {Zheng, Guolong and Bagheri, Hamid and Nguyen, ThanhVu},
	booktitle = {2020 IEEE International Conference on Software Maintenance and Evolution},
	publisher = {IEEE},
	pages = {844--848},
	title = {Debugging Declarative Models in Alloy},
	year = {2020}}

@inproceedings{nguyen2020usingc,
	author = {Nguyen, ThanhVu and Ishimwe$^3$, Didier and Malyshev$^2$, Alexey and Antonopoulos, Timos and Phan, Quoc-Sang},
	crossref = {nguyen2020using},
	note = {\href{https://roars.dev/pubs/nguyen2020using.pdf}{PDF}}}

@inproceedings{nguyen2020using,
	author = {Nguyen, ThanhVu and Ishimwe, Didier and Malyshev, Alexey and Antonopoulos, Timos and Phan, Quoc-Sang},
	booktitle = {International Workshop on Software Security from Design to Deployment},
	pages = {11--14},
	title = {Using Dynamically Inferred Invariants to Analyze Program Runtime Complexity},
	year = {2020}}

@article{mariano2019programc,
	crossref = {mariano2019program},
	note = {\href{https://roars.dev/pubs/mariano2019program.pdf}{PDF}},
	number = OOPSLA}

@article{mariano2019program,
	author = {Mariano, Benjamin and Reese, Josh and Xu, Siyuan and Nguyen, ThanhVu and Qiu, Xiaokang and Foster, Jeffrey S and Solar-Lezama, Armando},
	journal = {Proceedings of the ACM on Programming Languages},
	number = {OOPSLA},
	pages = {1--25},
	publisher = {ACM New York, NY, USA},
	title = {Program Synthesis with Algebraic Library Specifications},
	volume = {3},
	year = {2019}}

@inproceedings{le2019slingc,
	addendum = {Acceptance 27\%},
	author = {Le, TonChanh and Zheng$^3$, Guolong and Nguyen, ThanhVu},
	booktitle = PLDI,
	crossref = {le2019sling},
	note = {\href{https://roars.dev/pubs/le2019sling.pdf}{PDF}}}

@inproceedings{le2019sling,
	author = {Le, TonChanh and Zheng, Guolong and Nguyen, ThanhVu},
	booktitle = {Conference on Programming Language Design and Implementation},
	pages = {788--801},
	publisher = {ACM},
	title = {SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic},
	year = {2019}}

@inproceedings{zheng2018automaticc,
	author = {Zheng$^3$, Guolong and Le, Quang Loc and Nguyen, ThanhVu and Phan, Quoc-Sang},
	crossref = {zheng2018automatic},
	note = {\href{https://roars.dev/pubs/zheng2018automatic.pdf}{PDF}}}

@inproceedings{zheng2018automatic,
	author = {Zheng, Guolong and Le, Quang Loc and Nguyen, ThanhVu and Phan, Quoc-Sang},
	booktitle = {Java PathFinder Workshop},
	pages = {66--66},
	title = {{Automatic Data Structure Repair using Separation Logic}},
	year = {2018}}

@inproceedings{gazzillo2018localizingc,
	crossref = {gazzillo2018localizing},
	note = {\href{https://roars.dev/pubs/gazzillo2018localizing.pdf}{PDF}}}

@inproceedings{gazzillo2018localizing,
	author = {Gazzillo, Paul and Koc, Ugur and Nguyen, Thanhvu and Wei, Shiyi},
	booktitle = {International Systems and Software Product Line Conference (Challenge Track)},
	pages = {269-273},
	title = {{Localizing Configurations in Highly-Configurable Systems}},
	year = {2018}}

@inproceedings{nguyen2017counterexamplec,
	addendum = {Acceptance 24\%},
	booktitle = FSE,
	crossref = {nguyen2017counterexample},
	note = {\href{https://roars.dev/pubs/nguyen2017counterexample.pdf}{PDF}}}

@inproceedings{nguyen2017counterexample,
	author = {Nguyen, ThanhVu and Antonopoulos, Timos and Ruef, Andrew and Hicks, Michael},
	booktitle = {Foundations of Software Engineering},
	pages = {605--615},
	title = {Counterexample-guided approach to finding numerical invariants},
	year = {2017}}

@inproceedings{nguyen2017connectingc,
	addendum = {Acceptance 28\%},
	booktitle = TACAS,
	crossref = {nguyen2017connecting},
	note = {\href{https://roars.dev/pubs/nguyen2017connecting.pdf}{PDF}}}

@inproceedings{nguyen2017connecting,
	author = {ThanhVu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest},
	booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
	pages = {301--318},
	publisher = {Springer},
	title = {Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation},
	year = {2017}}

@inproceedings{nguyen2016igenc,
	addendum = {Acceptance 27\%},
	booktitle = FSE,
	crossref = {nguyen2016igen},
	note = {\href{https://roars.dev/pubs/nguyen2016igen.pdf}{PDF}}}

@inproceedings{nguyen2016igen,
	author = {Nguyen, ThanhVu and Koc, Ugur and Cheng, Javran and Foster, Jeffrey S. and Porter, Adam A.},
	booktitle = {Foundations of Software Engineering},
	keywords = {Program analysis; software testing; configurable systems},
	pages = {655--665},
	publisher = {ACM},
	title = {iGen: Dynamic Interaction Inference for Configurable Software},
	year = {2016}}

@inproceedings{nguyen2014usingc,
	addendum = {Acceptance 20\%},
	booktitle = ICSE,
	crossref = {nguyen2014using},
	note = {\href{https://roars.dev/pubs/nguyen2014using.pdf}{PDF}}}

@inproceedings{nguyen2014using,
	author = {Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie},
	booktitle = {International Conference on Software Engineering},
	pages = {608-619},
	publisher = {IEEE},
	title = {Using Dynamic Analysis to Generate Disjunctive Invariants},
	year = {2014}}

@inproceedings{nguyen2012usingc,
	addendum = {Acceptance 21\%},
	booktitle = ICSE,
	crossref = {nguyen2012using},
	note = {\href{https://roars.dev/pubs/nguyen2012using.pdf}{PDF}}}

@inproceedings{nguyen2012using,
	author = {Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie},
	booktitle = {International Conference on Software Engineering},
	pages = {683--693},
	publisher = {IEEE},
	title = {Using Dynamic Analysis to Discover Polynomial and Array Invariants},
	year = {2012},
    note_award = {ACM SIGSOFT Distinguished Paper Award}

    }
    

@article{nguyen2014digc,
	addendum = {Impact Factor 2.07\coe{, contribution 25\%}},
	crossref = {nguyen2014dig},
	journal = TOSEM,
	note = {\href{https://roars.dev/pubs/nguyen2014dig.pdf}{PDF}}}

@article{nguyen2014dig,
	author = {Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie},
	journal = {Transactions on Software Engineering Methodology},
	number = {4},
	pages = {30:1--30:30},
	publisher = {ACM},
	title = {{DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants}},
	volume = {23},
	year = {2014}}

@incollection{kapur2013geometricc,
	addendum = {\coe{contribution 16\%}},
	crossref = {kapur2013geometric},
	note = {\href{https://roars.dev/pubs/kapur2013geometric.pdf}{PDF}}}


@article{kapur2013geometric,
	author = {Kapur, Deepak and Zhang, Zhihai and Horbach, Matthias and Zhao, Hengjun and Lu, Qi and Nguyen, ThanhVu},
	booktitle = {Automated Reasoning and Mathematics: Essays in Memory of William W. McCune},
	pages = {189--228},
	publisher = {Springer},
	title = {{Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants}},
	volume = {7788},
	year = {2013}}

@article{le2011genprogc,
	addendum = {Impact Factor \tseif{}\coe{, contribution 25\%}},
	crossref = {le2011genprog},
	journal = TSE,
	note = {\href{https://roars.dev/pubs/le2011genprog.pdf}{PDF}}}

@article{le2011genprog,
	author = {Le Goues, Claire and Nguyen, ThanhVu and Forrest, Stephanie and Weimer, Westley},
	journal = {Transactions on Software Engineering},
	number = {1},
	pages = {54--72},
	publisher = {IEEE},
	title = {{Genprog: A Generic Method for Automatic Software Repair}},
	volume = {38},
	year = {2011},
    note_award = {IEEE TSE 50th Anniversary Retrospective Most Influential Paper Award}
    }

@article{weimer2010automaticc,
	addendum = {Impact Factor \cacmif\coe{, contribution 25\%}},
	crossref = {weimer2010automatic},
	journal = CACM,
	note = {\href{https://roars.dev/pubs/weimer2010automatic.pdf}{PDF}}}

@article{weimer2010automatic,
	author = {Weimer, Westley and Forrest, Stephanie and Le Goues, Claire and Nguyen, ThanhVu},
	journal = {Communications of the ACM},
	number = {5},
	pages = {109--116},
	publisher = {ACM New York, NY, USA},
	title = {{Automatic Program Repair with Evolutionary Computation}},
	volume = {53},
    year = {2010},
    note_award = {Research Highlight}
    }


@article{bui2008antc,
	addendum = {Impact Factor 0.99\coe{, contribution 25\%}},
	crossref = {bui2008ant},
	note = {\href{https://roars.dev/pubs/bui2008ant.pdf}{PDF}}}

@article{bui2008ant,
	author = {Bui, Thang and Nguyen, ThanhVu and Patel, Chirag and Phan, Kim-Anh},
	journal = {Discrete Applied Mathematics},
	keywords = {Graph coloring, Ant-based algorithm},
	number = {2},
	pages = {190--200},
	publisher = {Elsevier},
	title = {{An Ant-based Algorithm for Coloring Graphs}},
	volume = {156},
	year = {2008}}

@inproceedings{weimer2009automaticallyc,
	addendum = {Acceptance 12\%},
	booktitle = ICSE,
	crossref = {weimer2009automatically},
	note = {\href{https://roars.dev/pubs/weimer2009automatically.pdf}{PDF}}}

@inproceedings{weimer2009automatically,
	author = {Weimer, Westley and Nguyen, ThanhVu and {Le Goues}, Claire and Forrest, Stephanie},
    booktitle = ICSE,
	keywords = {software engineering, software repair, program analysis, program repair, genetic programming, evolutionary computing},
	pages = {364--367},
	publisher = {IEEE},
	title = {Automatically Finding Patches Using Genetic Programming},
	year = {2009},
    note_award = {
    ACM SIGSOFT Distinguished Paper Award;
    Manfred Paul Award for ExcellenceSoftware: Theory and Practice;
    ACM SIGSOFT 10-year Most Influential Paper Award}
    }

@inproceedings{forrest2009geneticc,
	addendum = {Acceptance 41\%},
	booktitle = GECCO,
	crossref = {forrest2009genetic},
	note = {\href{https://roars.dev/pubs/forrest2009genetic.pdf}{PDF}}}

@inproceedings{forrest2009genetic,
	author = {Forrest, Stephanie and Nguyen, ThanhVu and Weimer, Westley and Le Goues, Claire},
	booktitle = {Conference on Genetic and Evolutionary Computation},
	pages = {947--954},
	title = {A genetic programming approach to automated software repair},
	year = {2009},
    note_award = {Best Paper Award; ACM SIGEVO 10-year Impact Award}
    }

@inproceedings{bui2009parallelc,
	addendum = {Acceptance 41\%},
	booktitle = GECCO,
	crossref = {bui2009parallel},
	note = {\href{https://roars.dev/pubs/bui2009parallel.pdf}{PDF}}}

@inproceedings{bui2009parallel,
	author = {Bui, Thang and Nguyen, ThanhVu and {Rizzo Jr}, Joseph},
	booktitle = {Conference on Genetic and Evolutionary Computation},
	pages = {1--8},
	publisher = {ACM},
	title = {Parallel Shared Memory Strategies For Ant-based Optimization Algorithms},
	year = {2009},
    note_award = {Best Paper Award}
    }


@inproceedings{nguyen2009usingc,
	crossref = {nguyen2009using},
	note = {\href{https://roars.dev/pubs/nguyen2009using.pdf}{PDF}}}

@inproceedings{nguyen2009using,
	author = {Nguyen, ThanhVu and Weimer, Westley and {Le Goues}, Claire and Forrest, Stephanie},
	booktitle = {International Conference on Software Testing, Verification and Validation Workshops},
	pages = {152--153},
	publisher = {IEEE},
	title = {{Using Execution Paths to Evolve Software Patches}},
	year = {2009},
    note_award = {Best Short Paper Award and Best Presentation Award}
    }

@inproceedings{viamontes2007efficientc,
	crossref = {viamontes2007efficient},
	note = {\href{https://roars.dev/pubs/viamontes2007efficient.pdf}{PDF}}}

@inproceedings{viamontes2007efficient,
	author = {Viamontes, G and Amduka, M and Russo, J and Craven M and Nguyen, T},
	booktitle = {Annual High Performance Embedded Computing Workshop},
	publisher = {IEEE},
	title = {{Efficient Memoization Strategies for Object Recognition with a Multi-Core Architecture}},
	year = {2007},
    note_award = {Outstanding Submission}
    }

@inproceedings{smith2007fuzzyc,
	crossref = {smith2007fuzzy},
	note = {\href{https://roars.dev/pubs/smith2007fuzzy.pdf}{PDF}}}

@inproceedings{smith2007fuzzy,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	journal = {Signal Processing, Sensor Fusion, and Target Recognition XVI},
	publisher = {SPIE},
	title = {{Fuzzy Decision Trees for Planning and Autonomous Control of a Coordinated Team of UAVs}},
	year = {2007}}

@inproceedings{smith2007geneticc,
	crossref = {smith2007genetic},
	note = {\href{https://roars.dev/pubs/smith2007genetic.pdf}{PDF}}}

@inproceedings{smith2007genetic,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	journal = {Data Mining, Intrusion Detection, Information Assurance, and Data Networks Security 2007},
	publisher = {SPIE},
	title = {{Genetic Program based Data Mining of Fuzzy Decision Trees and Methods of Improving Convergence and Reducing Bloat}},
	year = {2007}}


@inproceedings{bui2006agentc,
	addendum = {Acceptance 46\%},
	booktitle = GECCO,
	crossref = {bui2006agent},
	note = {\href{https://roars.dev/pubs/bui2006agent.pdf}{PDF}}}

@inproceedings{bui2006agent,
	author = {Bui, Thang N and Nguyen, ThanhVu H},
	booktitle = {Conference on Genetic and Evolutionary Computation},
	pages = {19--26},
	title = {{An Agent-based Algorithm for Generalized Graph Colorings}},
	year = {2006}}

@inproceedings{smith2006guidingc,
	crossref = {smith2006guiding},
	note = {\href{https://roars.dev/pubs/smith2006guiding.pdf}{PDF}}}

@inproceedings{smith2006guiding,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {Intelligent Data Engineering and Automated Learning (IDEAL)},
	keywords = {Genetic Programs, Fuzzy Logic, Data Mining, Control Algorithms, Planning Algorithms.},
	pages = {1337--1345},
	publisher = {Springer},
	title = {{Guiding Genetic Program Based Data Mining Using Fuzzy Rules}},
	year = {2006}}

@inproceedings{smith2006evolutionaryc,
	crossref = {smith2006evolutionary},
	note = {\href{https://roars.dev/pubs/smith2006evolutionary.pdf}{PDF}}}

@inproceedings{smith2006evolutionary,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Conference on Informatics in Control Automation and Robotics (ICINCO)},
	keywords = {optimization problems in signal processing, signal reconstruction, system identification, time series and system modeling},
	pages = {107-113},
	publisher = {Springer},
	title = {Evolutionary Data Mining Approach to Creating Digital Logic},
	year = {2006}}

@inproceedings{smith2006fuzzy2c,
	crossref = {smith2006fuzzy2},
	note = {\href{https://roars.dev/pubs/smith2006fuzzy2.pdf}{PDF}}}

@inproceedings{smith2006fuzzy2,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Conference on Informatics in Control Automation and Robotics (ICINCO)},
	comment = {Also appears in Informatics in Control, Automation and Robotics, Lecture Notes in Electrical Engineering, Vol. 15(2), 2008, pp. 81-94.},
	keywords = {decision support systems, distributed control systems, fuzzy control, knowledge-based systems applications, software agents for intelligent control systems},
	pages = {81-94},
	publisher = {Springer},
	title = {Fuzzy Logic Based UAV Allocation and Coordination},
    note_award = {Best Paper Award},
	year = {2006}
    }

@inproceedings{smith2006fuzzyc,
	crossref = {smith2006fuzzy},
	note = {\href{https://roars.dev/pubs/smith2006fuzzy.pdf}{PDF}}}

@inproceedings{smith2006fuzzy,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {Annual Meeting of the North American Fuzzy Information Processing Society (NAFIPS)},
	pages = {463-470},
	publisher = {IEEE},
	title = {Fuzzy Logic Based Resource Manager for a Team of UAVs},
	year = {2006}}

@inproceedings{smith2006creatingc,
	crossref = {smith2006creating},
	note = {\href{https://roars.dev/pubs/smith2006creating.pdf}{PDF}}}

@inproceedings{smith2006creating,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {Annual Meeting of the North American Fuzzy Information Processing Society (NAFIPS)},
	pages = {471-477},
	publisher = {IEEE},
	title = {Creating Fuzzy Decision Algorithms Using Genetic Program Based Data Mining Program},
	year = 2006}

@inproceedings{smith2006resourcec,
	crossref = {smith2006resource},
	note = {\href{https://roars.dev/pubs/smith2006resource.pdf}{PDF}}}

@inproceedings{smith2006resource,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	journal = {Signal Processing, Sensor Fusion, and Target Recognition XV},
	keywords = {resource management, fuzzy logic, planning algorithms, decision support algorithms, cooperative behavior},
	pages = {118--129},
	publisher = {SPIE},
	title = {Resource Manager for an Autonomous Coordinated Team of UAVs},
	year = {2006}}

@inproceedings{smith2006geneticc,
	crossref = {smith2006genetic},
	note = {\href{https://roars.dev/pubs/smith2006genetic.pdf}{PDF}}}


@inproceedings{smith2006genetic,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	journal = {Data Mining, Intrusion Detection, Information Assurance, and Data Networks Security 2006},
	keywords = {data mining, knowledge discovery, genetic programs, genetic algorithms, reverse engineering, defect discovery},
	pages = {24-35},
	publisher = {SPIE},
	title = {Genetic Program based Data Mining to Reverse Engineer Digital Logic},
	year = {2006}}

@inproceedings{smith2005distributedc,
	crossref = {smith2005distributed},
	note = {\href{https://roars.dev/pubs/smith2005distributed.pdf}{PDF}}}

@inproceedings{smith2005distributed,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	journal = {Signal Processing, Sensor Fusion, and Target Recognition XIV},
	pages = {65--76},
	publisher = {SPIE},
	title = {Distributed Autonomous Systems: Resource Management, Planning, and Control Algorithms},
	year = {2005}}

@inproceedings{smith2005datac,
	crossref = {smith2005data},
	note = {\href{https://roars.dev/pubs/smith2005data.pdf}{PDF}}}

@inproceedings{smith2005data,
	author = {Smith III, James and Nguyen, ThanhVu},
	booktitle = {International Society for Optical Engineering},
	pages = {232--242},
	publisher = {SPIE},
	title = {Data Mining based Automated Reverse Engineering and Defect Discovery},
	year = {2005}}

@mastersthesis{nguyen2006graphc,
	crossref = {nguyen2006graph},
	note = {\href{https://roars.dev/pubs/nguyen2006graph.pdf}{PDF}}}

@mastersthesis{nguyen2006graph,
	author = {Nguyen, ThanhVu},
	keywords = {graph coloring, bandwidth coloring, multi-graph coloring, bandwidth multicoloring, ant-based algorithm},
	month = {12},
	organization = {Department of Computer Science},
	school = {The Pennsylvania State University},
	title = {On the Graph Coloring Problem and Its Generalizations},
	year = {2006}}

@article{smith2007autonomousc,
	addendum = {\coe{contribution 50\%}},
	crossref = {smith2007autonomous},
	note = {\href{https://roars.dev/pubs/smith2007autonomous.pdf}{PDF}}}

@article{smith2007autonomous,
	author = {Smith III, James F and Nguyen, ThanhVu H},
	journal = {Integrated Computer-Aided Engineering},
	number = {2},
	pages = {141--159},
	publisher = {IOS Press},
	title = {Autonomous and cooperative robotic behavior based on fuzzy logic and genetic programming},
	volume = {14},
	year = {2007}}

@phdthesis{nguyen2014automatingc,
	crossref = {nguyen2014automating},
	note = {\href{https://roars.dev/pubs/nguyen2014automating.pdf}{PDF}}
	}

@phdthesis{nguyen2014automating,
	author = {Nguyen, ThanhVu},
	keywords = {invariant generation, program synthesis, automatic program repair, test-input generation},
	month = {8},
	organization = {Department of Computer Science},
	school = {University of New Mexico},
	title = {Automating Program Verification and Repair Using Invariant Analysis and Test-input Generation},
	year = 2014}

@misc{digtool,
	author = {ThanhVu Nguyen},
	key = {digtool},
	url = {https://code.roars.dev/dig},
	title = {The DIG (Dynamic Invariant Generation) System}}
    }

@misc{neuralsattool,
	author = {Hai Duong and ThanhVu Nguyen},
	key = {neuralsattool},
	url = {https://code.roars.dev/neuralsat},
	title = {The NeuralSAT Verification Tool for Deep Neural Networks}
    }


@misc{csconfs,
	author = {},
	key = {csconfs},
	url = {https://roars.dev/csconfs},
	title = {CSConfs: A Webapp Showing CS Conferences Deadlines}
    }

@misc{cspicks,
	author = {},
	key = {cspicks},
	url = {https://roars.dev/cspicks},
	title = {CSPicks: A Webapp to Explore CS Programs and Professors}
    }

@unpublished{nwlgfunm,
	author = {T. Nguyen and W. Weimer and {Le Goues}, C and S. Forrest},
	note = {Poster, University of New Mexico Darwin's Legacy Symposium},
	title = {Evolving Software Repairs Using Genetic Programming},
	year = {2009}}

@unpublished{gca06,
	author = {ThanhVu Nguyen},
	note = {Penn State Graduate Research Exhibition},
	title = {Graphs Coloring with Ants},
	year = {2006}}

@unpublished{pcpctuav06,
	author = {ThanhVu Nguyen},
	note = {Poster, Penn State Graduate Research Exhibition},
	title = {Planning and Control Phases for Cooperative Teams of Unmanned Aerial Vehicles},
	year = {2006}}

@unpublished{reerec,
	author = {Thanhvu Nguyen},
	note = {Poster, Penn State Graduate Research Exhibition},
	title = {Reverse Engineering and Exploiting Radars through Evolutionary Computing},
	year = {2006}}

@unpublished{nwlgf,
	author = {T. Nguyen and W. Weimer and {Le Goues}, C and S. Forrest},
	keywords = {software engineering, software repair, program analysis, program repair, genetic programming, evolutionary computing},
	note = {University of New Mexico Computer Science Student Conference},
	title = {Fixing Real Software Bugs using Evolutionary Computing},
	url_paper = {csusc09.pdf},
	year = {2009}}

@unpublished{bgn08,
	author = {G. Bezerra and T. Nguyen},
	note = {University of New Mexico Computer Science Student Conference},
	title = {Modeling the Spread of Infection Diseases using an Agent-based Spatial Network},
	year = {2008}}

@misc{npbench,
	author = {Nguyen, Thanhvu and Bui, Thang},
	key = {benchmark},
	title = {DIMACS benchmarks repository: collections of benchmark instances for {NP-hard} problem},
	url = {https://code.roars.dev/npbench}
}

@misc{fnwlg-hc,
	author = {Forrest, S and Nguyen, T and Weimer, W and {Le Goues}, C},
	howpublished = {The 6th Annual Human-Computer "HUMMIES" Competition},
	keywords = {software engineering, software repair, program analysis, program repair, genetic programming, evolutionary computing},
	title = {Fixing Software Bugs in 10 Minutes or Less Using Evolutionary Computation},
	url_code = {http://www.genetic-programming.org/hc2009/cfe2009.html},
	url_slides = {Forrest-Presentation.pdf},
	year = {2009}}

@misc{nsf2023neuralsat,
	author = {Nguyen (sole-PI)},
	howpublished = {NSF \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2238133}{2238133}},
	keywords = {nsf-career},
	title = {CAREER: NeuralSAT: A Constraint-Solving Framework for Verifying Deep Neural Networks},
        organization={NSF},
	note = {8/1/2023--7/31/2028, \$510,509}
        }


@misc{nsf2024dig,
	author = {Nguyen (PI@GMU) and Kapur (PI@UNL)},
	howpublished = {NSF \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2422036}{2422036}},
	keywords = {nsf-fmit},
	title = {FMitF: Track II: Collaborative Research: FMitF: Track II: From Theory to Practice: Making Complex Invariants Accessible with DIG},
    organization={NSF},
	note = {9/1/2024--8/31/2026, \$150K (my portion: \$100K)}
}


@misc{nsf2023cybolic,
	author = {Nguyen (sole-PI)},
	howpublished = {NSF \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319131}{2319131}},
	keywords = {nsf-fmit},
	title = {FMitF: Track II: Cybolic: A Symbolic Execution Technique and Tool for Analyzing CMake Build Scripts},
    organization={NSF},
	note = {7/1/2023--1/30/2025, \$97,242}
        }

@misc{nsf2020kbuild,
	author = {Nguyen (sole-PI)},
	howpublished = {NSF  \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=1948536}{1948536};
 \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2304748}{2304748}},
	keywords = {nsf-funded1},
	title = {CRII: Analyzing Linux KBuild Makefiles},
        organization={NSF},
	note = {4/1/2020--3/31/2022, \$174,975}
        }



@misc{nsf2022dtemporal,
	author = {Nguyen (PI@GMU) and Koskinen (PI@Stevens) and Le (Co-PI@Stevens) and Antonopoulos (PI@Yale)},
	howpublished = {NSF \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2107035}{2107035};
        \href{https://www.nsf.gov/awardsearch/showAward?AWD_ID=2200621}{2200621}},
	keywords = {nsf-funded2},
	title = {Collaborative: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysis},
        organization={NSF},
	note = {7/15/2021--7/14/2024, \$1,199,871 (sole PI at GMU, my portion: \$399,879)}
        }


@misc{fb2022cmake,
	author = {Nguyen (sole-PI)},
	howpublished = {},
	title = {Analysis of CMake Build files using Symbolic Execution},
        organization={Facebook/WhatsApp},
	note = {2021, \$30,000  unrestricted gift}
        }


@misc{nvidia2025spark,
	author = {Nguyen (sole-PI)},
	howpublished = {},
	title = {NVIDIA Academic Grant Program},
        organization={NVIDIA},
	note = {2025, \href{https://www.nvidia.com/en-us/products/workstations/dgx-spark/}{DGX Spark System}}
        }

@misc{amz2023neuralsat,
	author = {Nguyen (sole-PI)},
	title = {Amazon Research Award (Automated Reasoning): Scalable and Precise DNN Constraint Solving with Abstraction and Conflict Clause Learning},
        organization={Amazon},
	note = {2023, \$50,000  unrestricted gift}
        }

@misc{aro2018predict,
	author = {Dwyer (PI) and Nguyen ({Co-PI})},
	howpublished = {ARO (W911NF1910054)},
	keywords = {nsf-funded1},
	title = {Predictive Failure Avoidance},
        organization={Army Research Office},
	note = {2018--2021, \$549,990 (my portion: \$158,850)}
        }


@misc{unl2021seed,
	author = {Nguyen (sole-PI)},
	keywords = {internal-funded2},
	title = {Faculty Seed Grant: Analyzing Highly-Configurable Software},
        organization={UNL},
	note = {2021, \$10K}
        }


@patent{bagheri2023systems,
  title={Systems, methods, and media for fault localization in declarative specification languages},
  author={Bagheri, Hamid and Nguyen, Thanhvu and Zheng, Guolong},
  year={2023},
  month={2},
  assignee={NuTech Ventures Inc},
  number={US Patent App. 17/887,827}
}




@misc{amazon202379,
  title = {79 Amazon Research Awards recipients announced},
  author = {Amazon Science},
  howpublished = {\url{https://www.amazon.science/research-awards/program-updates/79-amazon-research-awards-recipients-announced}},
  year = {2023}
}
@misc{thanhnien2023tiensi,
  title = {Tien Si Goc Viet Duoc Tai Tro Nghien Cuu AI},
  author={Thanh Nien News VN},
  howpublished = {\url{https://thanhnien.vn/tien-si-goc-viet-duoc-tai-tro-nghien-cuu-ai-185230304234603638.htm}},
  year = {2023}
}


@misc{gmu2025roars,
  title = {George Mason's ROARS lab retains its ranking as a leader in AI safety at the 2024 International Neural Network Verification Competition},
  author={GMU},
  howpublished = {\url{https://cec.gmu.edu/news/2025-05/george-masons-roars-lab-retains-its-ranking-leader-ai-safety-2024-international-neural}},
  year = {2025}
}


@misc{gmu2023amazon,
  title = {Amazon Research Award Win Ai Safety Verification},
  author={GMU},
  howpublished= {\url{https://cec.gmu.edu/news/2023-07/amazon-research-award-win-ai-safety-verification}},
  year={2023}
}

@misc{gmu2023boom,
  title = {Boom crash: Mason researcher receives half million NSF grant that could steer AI safely},
  author={GMU},
  howpublished = {\url{https://www.gmu.edu/news/2023-02/boom-crash-mason-researcher-receives-half-million-nsf-grant-could-steer-ai-safely}},
  year = 2023
}


@misc{unl2020nguyen,
  title = {Nguyen earns NSF CRII award},
  author={UNL},
  howpublished = {\url{https://computing.unl.edu/nguyen-earns-nsf-crii-award/}},
  year = {2020}
}

@misc{unl2019nguyen,
  title = {Nguyen earns ICSE 2019 Most Influential Paper Award},
  author={UNL},
  howpublished = {\url{https://computing.unl.edu/nguyen-earns-icse-2019-most-influential-paper-award/}},
  year = {2019}
}


@misc{sigbed2023neuralsat,
  title = {NeuralSAT: A CDCL-based constraint solving approach to DNN Verification},
  author={Nguyen, ThanhVu and Duong, Hai},
  howpublished = {\url{https://sigbed.org/2023/06/06/neural-sat/}},
  year = {2023}
}


@book{nguyen2025demystify,
  title={{Demystifying PhD Admissions in Computer Science: A Handbook for Navigating CS PhD Admissions in the U.S}},
  author={ThanhVu Nguyen},
  year={open-source},
  note={Open-source version available at \url{https://code.roars.dev/phd-cs-us/}},
  publisher={Amazon Kindle Direct Publishing},
  url={https://www.amazon.com/dp/B0F41HP6Y2}
}
@book{nguyensafe,
  title={{SAFE: Software Analysis and Formal rEasoning}},
  author={ThanhVu Nguyen},
  year={open-source},
  url={https://nguyenthanhvuh.github.io/class-oo/safe.pdf}
}


@book{nguyennnv,
  title={{Introduction to Neural Network Verification}},
  author={ThanhVu Nguyen and Hai Duong},
  year={open-source},
  url={https://roars.dev/book_nnv/book.pdf}
}