index.html

<!DOCTYPE html>
<html lang="en">

  <head>
    <meta charset="utf-8">
    <title>Roars Lab</title>
    <meta name="author" content="Roars@GMU--ThanhVu Nguyen">
    <meta name="description" content="Roars Lab at George Mason University">
    <meta name="keywords" content="Roars, ThanhVu Nguyen, AI Safety, DNN verification">
    <link rel="stylesheet" type="text/css" href="files/org.css">
    <link rel="icon" href="files/dino-ai.jpg">
  </head>

  <body>
    <div id="toc">📔 <b>CONTENTS</b>
      <div id="full">
        <a href="#news">News</a><br>      
        <a href="#people">People</a><br>
        <a href="#awards">Awards</a><br>
        <a href="#teaching">Teaching</a><br>
        <a href="#research">Research</a><br>
        <a href="#software">Software</a><br>
        <a href="#pubs">Publications</a><br>
        <a href="#miscs">Miscs</a><br>                
        <a href="#acknowledgement">Thanks!</a><br>
        <a href="#contact">Contact</a>
      </div>
    </div>

    <header>
      <div class="typewriter">
        <h1><abbr title="ROARS: Research on Automated Reasoning Systems">ROARS 🦖 Lab @ GMU</abbr></h1>
      </div>
      <table>
        <tr>
          <td>
            <figure>
              <img src="files/dino-ai.jpg" alt="AI-generated DinoROARS Mascot" title="AI-generated DynoRoars Mascot" width="150">
            </figure>
          </td>
          <td>
            <div class="myborder">
              <ul class="styled">
                <li data-icon="🏠 &nbsp;"><a href="https://cs.gmu.edu">Computer Science</a>, <a href="https://www.gmu.edu">George Mason University</a></li>
                <li data-icon="📆 &nbsp;">Weekly Meeting: 2:00 PM--3:30 PM Thurs, ENGR #4201</li>
                <li>
                    🖥️  &nbsp;Code: 
                    <a href="https://wiki.roars.dev">📝 &nbsp;Wiki</a>, &nbsp; 
                    <a href="https://git.roars.dev">Github repos</a>, &nbsp;  
                    <a href="https://github.com/dynaroars/dynaroars.github.io/">Webpage</a></li>
                <li><a href="#contact"> 📨 &nbsp;Contact</a>
                </li>
                <!-- <li data-icon="🌎 ">Zoom: <a href="https://gmu.zoom.us/j/93426386731">DynaRoars</a> (pw: 675238)</li> -->
              </ul>
            </div>
          </td>
        </tr>
      </table>
    </header>
    
    <p>Welcome to <b>ROARS</b> (Research on Automated Reasoning Systems) Lab at <a href="https://www.gmu.edu">George Mason University</a>. 
        We develop automated reasoning techniques to analyze and verify software and AI systems. See <a href="#research">Research</a> for more information.</p>

    <h2 id="news">News</h2>

    <div class="myborder">
      <ul>
        <li>4/2025: <b>CSConfs</b>: <a href="https://roars.dev/csconfs">https://roars.dev/csconfs/</a> is now live. This webapp tracks of upcoming CS conferences.</li>
        <li>4/2025: Demystifying PhD Admissions in Computer Science is now published and available through <a href="https://www.amazon.com/dp/B0F41HP6Y2">Amazon Kindle</a> (the book pdf will always be free through <a href="https://github.com/dynaroars/phd-cs-us">GitHub</a>).</li>
        <li>4/2025: Two <b>ISSTA'25</b> 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)</li>
        <li>4/2025: Elevated to IEEE Senior Member</li>
        <li>4/2025: <b>CAV'25</b> paper on the NeuralSAT DNN verification tool (👏 Hai)</li>
        <li>2/2025: <b>TSE</b> paper (50th Anniversary Special Issue) on Evolution of APR</li>
        <li>2/2025: 🏅 <b>TSE 10-Year Retrospective Most Influential Paper Award</b> for GenProg work on automatic program repair (with Claire, Wes, and Steph)</li>
        <li>1/2025: <a href="https://github.com/dynaroars/neuralsat">NeuralSAT</a> <b>ranked 2nd</b> overall in VNN-COMP'24 (our second participation, 👏 Hai).<br>

        <b>Note</b>: Initially VNN-COMP's script was not able to correctly parsed the output results of NeuralSAT. After fixing the issue, NeuralSAT's results were correctly parsed and NeuralSAT is placed 2nd in VNN-COMP'24. The <a href="https://www.arxiv.org/pdf/2412.19985">updated VNN-COMP’24 report</a> shows the updated rankings (e.g., Table B.1) and detailed results in Appendix B.</li>

        <li>1/2025: <b>ICSE'25</b> NIER paper on LLM-based autoformalization for LEAN (👏 Long, first paper)</li>
      </ul>
    </div>
    
    <details>
      <summary>Older News</summary>
      <div class="myborder">
        <ul>
            <li>8/2024: Appointed <b>Director</b> of the MS Software Engr program</li>
            <li>8/2024: Promoted to <b>Associate Professor</b> with <b>tenure</b></li>
            <li>6/2024: 🎁 Received an <b>NSF Collaborative Formal Methods in the Field (FMitF) Grant</b></li>
            <li>5/2024: 🏅 <b>Outstanding Undergraduate Research Award</b> from GMU (👏 Stefania)</li>
            <li>4/2024: <b>Nguyen</b> and <b>Long</b> joined as PhD students</li>
            <li>3/2024: <b>Stefania</b> joined as a undergraduate researcher</li>
            <li>2/2024: <b>FSE'24</b> research paper on new optimizations developed for the NeuralSAT DNN verification tool (👏 Hai, first research paper as first author)</li>
            <li>1/2024: <a href="https://github.com/dynaroars/neuralsat">NeuralSAT</a> ranked 4th overall and received the <b>New Participant Award</b> at VNN-COMP'23 (our first participation). It also won the <code>tllverifybench</code> category (👏 Hai and Linhan)</li>
            <li>1/2024: <b>Huong</b> joined as a undergraduate researcher</li>
    
          <li>11/2023: 🎉 Thanksgiving party!!!</li>
          <li>8/2023: <a href="https://github.com/dynaroars/neuralsat">NeuralSAT</a> <b>ranked 4th</b> overall in the annual Verifying Neural Network competition <a  href="https://sites.google.com/view/vnn2023">VNN-COMP'23</a> (our first participation, 👏 Hai and Linhan)</li>
          <li>8/2023: <b>FSE SRC</b> (Student Research Competition) paper on dynamic complexity analysis (👏 Didier)</li>
          <li>8/2023: <b>FSE'23</b> Industry paper on fault localization</li>
          <li>7/2023: 🎁 Received an <b>NSF Formal Methods in the Field (FMitF) Grant</b></li>
          <li>7/2023: 📓 A handbook for <a href="https://dynaroars.github.io/phd-cs-us/demystify.pdf">demystifying the Ph.D. admission process in Computer Science in the US</a></li>
          <li>6/2023: SIGBED <a href="https://sigbed.org/2023/06/06/neural-sat/">blog</a> on NeuralSAT</li>
          <li>5/2023: 🏅 <b>Outstanding Undergraduate Senior Award</b> from UNL CSE (👏  KimHao)</li>
          <li>3/2023: 🎁 Received an <b>Amazon Research Award</b>. Press: <a href="https://www.amazon.science/research-awards/program-updates/79-amazon-research-awards-recipients-announced">Amazon Science</a>, <a href="https://cec.gmu.edu/news/2023-07/amazon-research-award-win-ai-safety-verification">GMU</a></li>
          <li>1/2023: 🎁 Received the <b>NSF CAREER Award</b> to work on DNN verification. Press: <a href="https://www.gmu.edu/news/2023-02/boom-crash-mason-researcher-receives-half-million-nsf-grant-could-steer-ai-safely">GMU</a>, <a href="https://thanhnien.vn/tien-si-goc-viet-duoc-tai-tro-nghien-cuu-ai-185230304234603638.htm">Báo Thanh Niên (Vietnamese)</a></li>
          <li>12/2022: <b>ICSE SEIP</b> paper on shift left static analysis (👏 KimHao)</li>
          <li>11/2022: 🎉 Thanksgiving party!!!</li>
          <li>11/2022: <b>SIGMOD'23</b> research paper on using graph neural networks to analyze IoT interactive bugs</li>
          <li>8/2022: 🎉 Start of the semester party!!!</li>
          <li>8/2022: <b>Hai</b> joined as a Ph.D. student</li>
          <li>7/2022: <b>ASE'22</b> research paper on feed-back driven iterative Alloy repair (👏 Guolong)</li>
          <li>4/2022: 🎓 <b>Guolong</b> defended his dissertation on Alloy analysis (first Ph.D. alumni of the group!)</li>
          <li>4/2022: <b>ISSTA'22</b> research paper on template-based Alloy repair (👏 Guolong)</li>
          <li>1/2022: Two <b>ICSE Tool</b> papers on complex analysis (👏 Didier) and invariant generation (👏 KimHao and Hai)</li>
          <li>1/2022: <b>ICSE SEIP</b> paper on analyzing CMake build scripts (👏 KimHao)</li>
          <li>1/2022: <b>Linhan</b> joined as a Ph.D. student</li>          
          <li>12/2021: <b>ICSE NIER</b> paper on Graph Neural Networks analysis</li>
          <li>9/2021: <b>OOPSLA'21</b> research paper on capturing runtime complexity of recursive programs (👏 Didier and KimHao)</li>
          <li>9/2021: <b>TSE'21</b> journal paper on symbolic states and dynamic invariant inference (👏 KimHao)</li>        
          <li>8/2021: 🎁 Received a gift from <b>Meta/Facebook</b> to work on build systems and symbolic execution</li>
          <li>8/2021: 🎁 Received an <b>NSF Collaborative (Medium) Grant</b> to dynamically analyze program liveness and safety properties</li>
          <li>8/2021: 🎉 Farewell party!!!</li>
          <li>7/2021: Three <b>ASE Tool papers</b> (👏 KimHao and Guolong)</li>        
          <li>6/2021: 🚀 Moving to <b>George Mason University</b> (Fall'21)</li>
          <li>5/2021: 🏅 <b>Outstanding Undergraduate Research Assistant Award</b> from UNL CSE (👏 KimHao)</li>
          <li>5/2021: 🎓 <b>Alexey</b> defended his Master's thesis</li> 
          <li>4/2021: 🏅 KimHao received the <b>Top Presentation Award</b> on analyzing configurable systems at the Nebraska Student Research Days</li>
          <li>12/2020: <i>Three</i> research papers accepted at <b>ICSE'21</b> on inferring interactions in
            configurable software and debugging and repairing Alloy specifications (👏 KimHao and Guolong)
          </li>
          <li>12/2020: 🎁 Received a <b>Faculty Seed Grant Award</b> from UNL</li>
          <li>10/2020: <b>OOPSLA'20</b> research paper on using dynamically inferred nonlinear invariants to prove program termination and non-termination</li>
          <li>9/2020: 🎁 <b>UCare Award</b> from UNL and the <b>Garmin Scholarship Award</b> (👏 KimHao)</li>
          <li>8/2020: <b>FSE SEAD</b> workshop paper on using recurrence relations to analyze program complexity (👏 Alexey and Didier)</li>
          <li>7/2020: <b>ICSME</b> NIER paper on using symbolic execution to analyze the Linux build system (👏 KimHao)</li>
          <li>7/2020: <b>ICSME</b> Doctoral Symposium paper on Alloy fault
            localization and repair (👏 Guolong)</li>
          <li>3/2020: 🎁 Received the <b>NSF CISE Research Initiation Initiative (CRII) Award</b> on analyzing the Linux build system.
            Press: <a href="https://computing.unl.edu/nguyen-earns-nsf-crii-award/">UNL</a></li>
          <li>3/2020: <b>KimHao</b> (freshman) joined as an undergraduate researcher</li>
          <li>1/2020: <b>Alexey</b> joined as an M.S. student</li>
          <li>9/2019: <b>OOPSLA'19</b> research paper on using algebraic specifications to aid program synthesis</li>
          <li>9/2019: <b>Didier</b> joined as a Ph.D. student</li>        
          <li>6/2019: 🏅🏅 Received an <b>ACM SIGSOFT 10-year Most Influential Paper Award</b> at ICSE
            (Software Engr) on program repair. Also an <b>ACM SIGEVO 10-year Impact Award</b>
            at GECCO (Evolutionary Computing) on using genetic programming to fix
            bugs</li>
          <li>3/2019: <b>PLDI'19</b> research paper on dynamic invariant inference in separation logic (👏 Guolong)</li>
          <li>1/2019: 🎁 Received a 3-year grant from the <b>Army Research Office</b> to work on program errors prediction and avoidance</li>
        </ul>
      </div>
    </details>
    

    <hr>

    <h2 id="people">People</h2>
    
    <p><a href="https://photos.roars.dev">Lab activities/photos</a></p>
    <div class="myborder">
      <ul>
        <li><a href="https://tvn.roars.dev">ThanhVu Nguyen</a> (faculty)</li>
        <li>Alex (Habeen) Chang (Ph.D. student)</li>        
        <li><a href="https://longdct.github.io">Long Doan</a> (Ph.D. student)</li>
        <li><a href="https://hocdot.github.io/">Hai Duong</a> (Ph.D. student)</li>        
        <li><a href="https://ishimwed.github.io">Didier Ishimwe</a> (Ph.D. student)</li>
        <li>Nguyen Ho (Ph.D. student)</li>
        <li>Linhan Li (Ph.D. student)</li>
        <li>Stefania Piciorea (undergraduate)</li>
      </ul>
    </div>    
    
    <details>
      <summary>Alumni</summary>
      <div class="myborder">      
        <ul>
          <li><a href="https://ndkimhao.github.io/">KimHao Nguyen</a> (B.S., <b>graduated 2023</b>, Jump Trading)</li>        
          <li><a href="https://scholar.google.com/citations?user=FqXt_DQAAAAJ">Guolong Zheng</a> (Ph.D., <b>graduated 2022</b>, A10 Networks)</li>
          <li>Alexey Malyshev (M.S., <b>graduated 2021</b>, Oracle)</li>
        </ul>
      </div>
    </details>
    
    
    <details>
      <summary><b>Join us</b>: Interested in our research in <b>safe and robust AI</b> and <b>software analysis?</b></summary>
      <div class="myborder">
        <ul>
          <li>Read <em>"Should you contact a US professor? How to do so correctly?"</em> from the <a href="https://github.com/dynaroars/phd-cs-us/">CS PhD Admission Demystify Handbook</a>. Also read <a href="https://go.gmu.edu/cs-stats">why you would want to join CS@GMU</a>.
          <li><a href="#contact">Email</a> the following:
            <ul>
              <li>Why are you interested in working with us? <strong>Be as specific as possible</strong>, e.g., you have read our papers or if you have worked on something related, discuss them.
                We <strong>will not</strong> read or reply to your email if it is generic (i.e., could be sent to multiple professors)
              <li><b>Do</b> the following programming assignments <a href="https://github.com/nguyenthanhvuh/class-verification/wiki/PA1">PA1</a> and <a href="https://github.com/nguyenthanhvuh/class-verification/wiki/PA2">PA2</a>. 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.</li>
              <li>Put <strong>"Roars Lab Applicant"</strong> in the subject line of the email</li>
              <li>Send your email using plain text (no colors or fancy fonts). <strong>Do not</strong> send your transcript, GRE, or any other scores.
            </ul>
        <li><strong>Note that we might not be able to respond to all mails received, especially those that might not fit our lab</strong>. However, we still encourage you to apply to GMU (<a href="https://go.gmu.edu/cs-stats">why?</a>) and mention our lab in your SOP.
        </ul>
    </div>
    </details>

    <hr>
    <h2 id="awards">Awards</h2>
    <div class="myborder">    
      <ul>
        <li><b>IEEE TSE 50th Anniversary Retrospective Most Influential Paper Award</b> 2025</li>
        <li>NeuralSAT ranked <b>2nd</b> overall in <b>VNN-COMP'24</b></li>        
        <li><b>Outstanding Undergraduate Research Award</b> 2024 (Stefania@GMU)</li>
        <li>NeuralSAT received the <b>New Participant Award</b> at VNN-COMP'23</li>
        <li><b>Outstanding Undergraduate Senior Award</b> 2023 (KimHao@UNL)</li>
        <li><a href="https://www.amazon.science/research-awards/program-updates/79-amazon-research-awards-recipients-announced"><b>Amazon Research Award</b> (Automated Reasoning)</a> 2023</li>
        <li><b>NSF CAREER</b> 2023</li>
        <li><b>Outstanding Undergraduate Researcher Award</b> 2021 (KimHao@UNL)</li>
        <li>NSF CISE Research Initiation Initiative (C<b>RII</b>) 2020</li>
        <li><a href="https://sig.sigevo.org/index.html/tiki-index.php?page=SIGEVO+Impact+Award">ACM SIGEVO <b>10-year Impact Paper Award</b></a> 2019</li>
        <li><a href="https://www.sigsoft.org/awards/icseMIPAward.html">ACM SIGSOFT / IEEE TCSE ICSE <b>10-year Most Influential Paper Award</b></a> 2019</li>
      </ul>
    </div>
    
    <details>
      <summary>Press Release</summary>
      <div class="myborder">
        <ol>
          <li><a href="https://cec.gmu.edu/news/2023-07/amazon-research-award-win-ai-safety-verification">Amazon Research Award Win for AI Safety Verification</a>: GMU press release on the ARA</li>
          <li><a href="https://www.gmu.edu/news/2023-02/boom-crash-mason-researcher-receives-half-million-nsf-grant-could-steer-ai-safely">Boom crash: Mason researcher receives half million NSF grant that could steer AI safely</a>: GMU press release on CAREER award</li>
          <li><a href="https://thanhnien.vn/tien-si-goc-viet-duoc-tai-tro-nghien-cuu-ai-185230304234603638.htm">Tiến sĩ gốc Việt được tài trợ nghiên cứu AI</a>: from Thanh Nien, a Vietnamese news outlet</li>
          <li><a href="https://computing.unl.edu/nguyen-earns-nsf-crii-award/">CRII Award</a>: UNL press release on NSF CRII award</li>
          <li><a href="https://newsroom.unl.edu/announce/cse/9518/56343">UNL press release</a> on ACM SIGSOFT 10-year Most Influential Paper Award at ICSE</li>
        </ol>
      </div>
    </details>

    <hr>
    <h2 id="teaching">Teaching</h2>

    <div class="myborder">
      <ul>
        <li>
          <a href="https://nguyenthanhvuh.github.io/class-oo/">OO Software Specification and Construction: SWE 419/619</a>
          (<a href="people/nguyenthanhvuh/files/feedback_oospecs.txt">student feedback</a>)
        </li>
      </ul>
    </div>

    <details>
      <summary>Previous</summary>
      <div class="myborder">
        <ul>
          <li>
            AI Safety and Assurance: CS 695
          </li>

          <li>
            Compilers: CSCE 425/825
            (<a href="people/nguyenthanhvuh/files/feedback_compilers.txt">student feedback</a>)
          </li>
          <li>
            Software Testing, Verification, and Analysis: CSCE 467/867
            (<a href="people/nguyenthanhvuh/files/feedback_tva.txt">student feedback</a>)
          </li>
          <li>Automata, Computation, and Formal Languages</li>
          <li>
            Software Engineering II (Specification and analysis of complex software systems)
          </li>
          <li>
            Software Verification (or Ensuring Software Dependability) Seminar: CSCE 990
          </li>
        </ul>
      </div>
    </details>


    <hr>

    <h2 id="research">Research</h2>

    <p>Software Engineering; Formal Methods; Automated Reasoning; Program Analysis; Program Verification; AI Safety and Robustness, Dynamic and Static Analysis; SMT/SAT Solving</p>


    <div class="myborder">
      <ul>
        <li><b>Safe and Robust AI</b>: we are exploring scalable and precise techniques
          to formally analyze and verify deep neural networks (DNNs).
          <ul>
            <li>Examples: <a href="https://arxiv.org/pdf/2307.10266.pdf">DPLL(T)-based DNN Verification</a></li>
          </ul>
        </li>

        <li><b>Program Analysis and Invariants Discovery</b>: we have developed dynamic, static, and
          symbolic techniques to analyze program semantics and to discover and prove interesting properties.
          <ul>
            <li>Examples: discovering <a href="./pubs/nguyen2012using.pdf">nonlinear
                polynomial invariants</a> using dynamic analysis (<b>ICSE Distinguished Paper
                Award</b>); discovering heap-based memory properties using
              <a href="./pubs/le2019sling.pdf">separation logic</a>; generating
              program interactions in highly-configurable software using
              <a href="./pubs/nguyen2021gentree.pdf">decision trees</a></li>
          </ul>
        </li>

        <li><b>Fault Localization and Automated Program Repair</b>: 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.
          <ul>
            <li>Examples: C program repair using <a href="pubs/nguyen2017connecting.pdf">symbolic testing</a> and <a href="./pubs/le2011genprog.pdf">genetic programming</a>
              (<b>10-year ICSE Most Influential Paper Award</b>); localizing faults in model specifications using <a href="./pubs/zheng2021flack.pdf">counterexamples</a></li>
          </ul>
        </li>
        <li><b>LSP-based IDEs</b>: we create extension to bring automated reasoning capabilities to IDEs such as VSCode.
        </li>
      </ul>
    </div>

    <h3 id="software"><a href="https://github.com/dynaroars">Software</a></h3>

    <div class="myborder">
      <ul>
        <li><a href="https://roars.dev/csconfs">CSConfs</a>: a webapp to track upcoming CS conferences.</li>
        <li><a href="https://github.com/dynaroars/neuralsat">NeuralSAT</a>: A high-performance <b>deep neural network (DNN) verification</b> tool.</li>
        <li><a href="https://github.com/dynaroars/dig">DIG</a>: A <b>numerical invariant generation tool</b>, focusing on nonlinear polynomials</li>
      </ul>
    </div>

    <details>
      <summary>More</summary>
      <div class="myborder">
        <ul>
          <li><a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main/c/nla-digbench">NLA-Digbench</a>: this
            SV-COMP benchmark contains various program with nonlinear invariants and properties.</li>
          <li>Solving NP-Complete problems
            <ul>
              <li><a href="https://github.com/dynaroars/coloring/">AntColor</a>: an ant-based heuristics for the <b>graph coloring</b> problem and its generalizations</li>
              <li><a href="https://github.com/dynaroars/maxclique/">AMC</a>: a fast, parallel ant-based algorithm for the <b>maximum clique</b> problem</li>
              <li><a href="https://github.com/dynaroars/npbench">NP Benchmarks</a>:  a comprehensive collection of benchmarks (in DIMACS format) for various NP-Complete problems including graph coloring, maximum clique, vertex cover, and spanning tree</li>
            </ul>
          </li>
        </ul>
      </div>
    </details>


    <hr>


<h2 id="pubs">Publications</h2>

<h3><a href="https://scholars.roars.dev">Google Scholars for Roars</a></h3>

<h3 id="miscs">Miscs Writing</h3>

<div class="myborder">
  <ol>
  <li>📚  A <a href="https://github.com/dynaroars/phd-cs-us/">book</a> to help students understand and navigate the Ph.D. admission process in Computer Science in the US</li>

    <li>📍 <a href="https://go.gmu.edu/cs-stats">https://go.gmu.edu/cs-stats</a>: Useful Stats about GMU CS dept</li>
    <li>📍 <a href="https://go.gmu.edu/viet-cs-profs-us">https://go.gmu.edu/viet-cs-profs-us</a>: Vietnamese professors in CS</li>
  </ol>
</div>


<h3>Unpublished/Under Submission</h3>

<div class="myborder">
  <ol>
    <li>Hai Duong, ThanhVu Nguyen, Matthew Dwyer, <a href="https://arxiv.org/pdf/2307.10266.pdf">A DPLL(T) Framework for Verifying Deep Neural Networks</a>, Arxiv</li>
    <li>Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos, Eric Koskinen, ThanhVu Nguyen, <a href="https://arxiv.org/abs/2306.15584v1">DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing</a>, Arxiv</li>
  </ol>
</div>

<h3>Published/To-appear Papers</h3>
<ul>
  <li><em>Emphasized author names</em>: Roars' students</li>
  <li><b>Bold conference or journal names</b>: full technical papers at top conferences or journals</li>
</ul>


<div class="myborder">
  <ol>
    <li><em>Stefania Piciorea</em> and Thanhvu Nguyen.
        <a href="pubs/piciorea2025bringing.pdf">Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code</a>. 
        ISSTA-Tool Demo, 2025</li>

    <li><em>Linhan Li</em> and ThanhVu Nguyen.
        COOLer: A Language Support Extension for COOL in VS Code.
        ISSTA-Tool Demo, 2025</li>

    <li><em>Hai Duong</em>, ThanhVu Nguyen, Matthew Dwyer.
        NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks.
        <b>Computer Aided Verification (CAV)</b>, 2025</li>

    <li>Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. The Evolution of Automated Software Repair.
         <b>Transactions on Software Engineering (TSE)</b>, 2025</li>
    <li><em>Long Doan</em> and ThanhVu Nguyen.
	    <a href="pubs/doan2025ai.pdf">AI-Assisted Autoformalization of Combinatorics Problems in Proof Assistants</a>.
        International Conference on Software Engineering- New Idea and Emergining Results (ICSE-NIER), 2025</li>
  
    <li><em>Hai Duong</em>, Dong Xu, ThanhVu Nguyen, Matthew Dwyer.
      <a href="pubs/duong2024harnessing.pdf">Harnessing Neuron Stability to Improve DNN Verification</a>,
      <b>Foundations of Software Engineering (FSE)</b>. 859--881, 2024</li>

    <li><em>Didier Ishimwe</em>. Inferring Complexity Bounds from Recurrence Relations. 
        Foundations of Software Engineering (Student Research Competition). 2023</li>

    <li>Tung Dao, Na Meng, and ThanhVu Nguyen.
      <a href="pubs/dao2013triggering.pdf">Triggering Modes in Spectrum-Based Multi-Location Fault Localization</a>,
          <b>Foundations of Software Engineering (FSE) Industry Track</b>. 1774--1785, 2023</li>

        <li>ThanhVu Nguyen and <em>Hai Duong</em>.
          <a href="https://sigbed.org/2023/06/06/neural-sat">NeuralSAT: A CDCL-based constraint solving approach to DNN Verification</a>.
          SIGBED Blog, 2023</li>

        <li>Quoc-Sang Phan, <em>KimHao Nguyen</em>, ThanhVu Nguyen.
          <a href="pubs/phan2023challenges.pdf">Challenges in Shift Left Static Analysis</a>,
          International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), 340--342, 2023</li>

        <li>Guangjing Wang, Nikolay Ivanov, Bocheng Chen, Qi Wang, ThanhVu Nguyen, Qiben Yan,
          <a href="pubs/wang2023graph.pdf">Graph Learning for Interaction Analysis in Smart Home Rule Data</a>,
          <b>ACM SIGMOD</b>,1--27, 2023</li>

        <li>Simón Gutiérrez Brida, Germán Regis, <em>Guolong Zheng</em>,
          Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias.
          <a href="pubs/brida2022icebar.pdf">ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications</a>,
          <b>Automated Software Engineering (ASE)</b>, pages 1--13, 2022</li>

        <li><em>Guolong Zheng</em>, ThanhVu Nguyen, Simón Gutiérrez Brida,
          Germán Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri.
          <a href="pubs/zheng2022atr.pdf">ATR: Template-based Repair for Alloy Specifications</a>,
          <b>International Symposium on Software Testing and Analysis (ISSTA)</b>, pages 666--677, 2022
        </li>

        <li><em>KimHao Nguyen</em>, ThanhVu Nguyen, and Quoc-Sang Phan.
          <a href="pubs/nguyen2022analyzing.pdf">Analyzing the CMake Build System</a>.
          International Conference on Software Engineering-Software Engineering in Practice (ICSE-SEIP), pages 27--28, 2022</li>

        <li>Thanh-Dat Nguyen, Thanh Le Cong, ThanhVu Nguyen, Bach Le, and Huynh Quyet Thang.
          <a href="pubs/nguyen2022toward.pdf">Toward the Analysis of Graph Neural Network</a>.
          International Conference on Software Engineering- New Idea and Emergining Results (ICSE-NIER), pages 116–-120, 2022</li>


        <li><em>Didier Ishimwe</em>, <em>KimHao Nguyen</em>, and ThanhVu Nguyen.
          <a href="pubs/ishimwe2022dynaplex.pdf">Dynaplex: Inferring Asymptotic Runtime Complexity of Recursive Programs</a>.
          International Conference on Software Engineering- Tool Demo, pages 61--64, 2022</li>


        <li>ThanhVu Nguyen, <em>KimHao Nguyen</em>, and <em>Hai Duong</em>.
          <a href="pubs/nguyen2022syminfer.pdf">SymInfer: Inferring Numerical Invariants using Symbolic States</a>.
          International Conference on Software Engineering-Tool Demo, pages 197--201, 2022</li>

        <li><em>Didier Ishimwe</em>, <em>KimHao Nguyen</em>, and ThanhVu Nguyen.
          <a href="pubs/ishimwe2021dynaplex.pdf">Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations</a>,
          <b>Proc. ACM Program. Lang. (OOPSLA)</b>, pages 1--23, 2021
        </li>
        <li>ThanhVu Nguyen, <em>KimHao Nguyen</em>, Matthew Dwyer.
          <a href="pubs/nguyen2021using.pdf">Using Symbolic States to Infer Numerical Invariants</a>,
          <b>Transactions on Software Engineering (TSE)</b>, 2021</li>

        <li><em>KimHao Nguyen</em> and ThanhVu Nguyen.
          <a href="pubs/nguyen2021gentree.pdf">GenTree: Using   Decision Trees to Learn Interactions for Configurable Software</a>.
          <b>International Conference on Software Engineering (ICSE)</b>, pages 1598–-1609,
          2021. <a href="pubs/nguyen2021artifact.pdf">Artifact Evaluation</a></li>

        <li><em>Guolong Zheng</em>, ThanhVu Nguyen, Simón Gutiérrez Brida,
          Germán Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri,
          <a href="pubs/zheng2021flack.pdf">FLACK: Counterexample-Guided Fault Localization for Alloy Models</a>,
          <b>International Conference on Software Engineering (ICSE)</b>, pages 637-–648, 2021.
          <a href="pubs/zheng2021artifact.pdf">Artifact Evaluation</a></li>

        <li>Simón Gutiérrez Brida, Germán Regis, <em>Guolong Zheng</em>,
          Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias.
          <a href="pubs/brida2021bounded.pdf">Bounded Exhaustive Search of
            Alloy Specification Repairs</a>,
          <b>International Conference on Software Engineering (ICSE)</b>, pages 1135–-1147, 2021.
          <a href="pubs/brida2021artifact.pdf">Artifact Evaluation</a>
        </li>

        <li><em>KimHao Nguyen</em> and ThanhVu Nguyen. <a href="pubs/nguyen2021tool.pdf">GenTree: Inferring
            Configuration
            Interactions using Decision Trees</a>. Automated Software Engineering
          (ASE Tool paper), 2021.</li>

        <li><em>Guolong Zheng</em>, ThanhVu Nguyen, Simón Gutiérrez Brida,
          Germán Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri,
          <a href="pubs/zheng2021tool.pdf">FLACK: Localizing Faults in Alloy Models</a>,
          Automated Software Engineering (ASE Tool paper), 2021.</li>

        <li>Simón Gutiérrez Brida, Germán Regis, <em>Guolong Zheng</em>,
          Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias.
          <a href="pubs/brida2021tool.pdf">BeAFix: An Automated Repair Tool for
            Faulty Alloy Models</a>,
          Automated Software Engineering (ASE Tool paper), 2021. </li>


        <li>Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric
          Koskinen, and ThanhVu Nguyen. <a href="pubs/le2020dynamite.pdf">DynamiTe: Dynamic Termination and
            Non-termination Proofs</a>. <b>Proc. ACM Program. Lang.
            (OOPSLA)</b>, vol 4, pages 1–30, 2020.</li>
        <li>ThanhVu Nguyen, <em>Didier Ishimwe</em>, <em>Alexey
            Malyshev</em>, Timos Antonopoulos, and Quoc-Sang Phan. <a href="pubs/nguyen2020using.pdf">Using
            Dynamically
            Inferred Invariants
            to Analyze Program Runtime Complexity</a>. Foundations of Software
          Engineering, Workshop on Software Security from Design to Deployment
          (FSE SEAD), pages 11–14, 2020.</li>
        <li><em>Guolong Zheng</em>, Hamid Bagheri and Thanhvu Nguyen. <a
                                                                        href="pubs/zheng2020debugging.pdf">Debugging
            Declarative Models in
            Alloy</a>. International Conference on Software Maintenance and
          Evolution, Doctoral Symposium (ICSME), pages 844–848, 2020.</li>
        <li>ThanhVu Nguyen and <em>KimHao Nguyen</em>. <a href="pubs/nguyen2020using2.pdf">Using Symbolic
            Execution to
            Analyze
            Linux KBuild Makefiles</a>. International Conference on Software
          Maintenance and Evolution, New Ideas and Emerging Results (ICSME NIER),
          pages 712–-716, 2020.</li>

        <li>Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang
          Qiu, Jeffrey S. Foster, and Armando Solar-Lezama. <a href="pubs/mariano2019program.pdf">Program
            Synthesis with
            Algebraic
            Library Specifications</a>. <b>Proc. ACM Program. Lang.
            (OOPSLA)</b>, vol 3, pages 1–25, 2019.</li>
        <li>Ton Chanh Le, <em>Guolong Zheng</em>, and ThanhVu Nguyen. <a href="pubs/le2019sling.pdf">SLING:
            Using Dynamic
            Analysis to Infer
            Program Invariants in Separation Logic</a>.
          <b>Programming Language Design and Implementation (PLDI)</b>, pages 788–-801. ACM,
          2019.</li>
        <li><em>Guolong Zheng</em>, Quang Loc Le, ThanhVu Nguyen, and
          Quoc-Sang Phan. <a href="pubs/zheng2018automatic.pdf">Automatic data
            structure repair using separation logic</a>. Java PathFinder Workshop,
          pages 66–-66, 2018.</li>
        <li>Paul Gazzillo, Ugur Koc, Thanhvu Nguyen, and Shiyi Wei. <a
                                                                      href="pubs/gazzillo2018localizing.pdf">Localizing
            Configurations in
            Highly-Configurable Systems</a>. International Systems and Software
          Product Line Conference, Challenge Track (SPLC), pages 269–-273,
          2018.</li>
        <li>ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks.
          <a href="pubs/nguyen2017counterexample.pdf">A Counterexample-guided
            Approach to Finding Numerical Invariants</a>. <b>Foundations of
            Software Engineering (FSE)</b>, pages 605–-615. ACM, 2017.
        </li>
        <li>ThanhVu Nguyen, Matthew Dwyer, and William Visser.
          <a href="pubs/nguyen2017syminfer.pdf">SymInfer: Inferring Program Invariants using Symbolic States</a>.
          <b>Automated Software Engineering (ASE)</b>, pages 804–-814. IEEE, 2017.</li>
        <li>ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie
          Forrest. <a href="pubs/nguyen2017connecting.pdf">Connecting Program
            Synthesis and Reachability: Automatic Program Repair using Test-Input
            Generation</a>. <b>International Conference on Tools and Algorithms
            for the Construction and Analysis of Systems (TACAS)</b>, pages
          301–-318. Springer, 2017.</li>
        <li>ThanhVu Nguyen, Ugur Koc, Javran Cheng, Jeffrey S. Foster, and
          Adam A. Porter. <a href="pubs/nguyen2016igen.pdf">iGen: Dynamic
            Interaction Inference for Configurable Software</a>. <b>Foundations
            of Software Engineering (FSE)</b>, pages 655–-665. ACM,
          2016.</li>
        <li>ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie
          Forrest. <a href="pubs/nguyen2014dig.pdf">DIG: A Dynamic Invariant
            Generator for Polynomial and Array Invariants</a>. <b>Transactions
            on Software Engineering Methodology (TOSEM)</b>, 23(4):30:1–-30:30,
          2014.</li>
        <li>ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie
          Forrest. <a href="pubs/nguyen2014using.pdf">Using Dynamic Analysis to
            Generate Disjunctive Invariants</a>. <b>International Conference on
            Software Engineering (ICSE)</b>, pages 608-–619. IEEE,
          2014.</li>
        <li>Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi
          Lu, and ThanhVu Nguyen. <a href="pubs/kapur2013geometric.pdf">Geometric
            Quantifier Elimination Heuristics for Automatically Generating Octagonal
            and Max-plus Invariants</a>. Automated Reasoning and Mathematics (Essays
          Memory of William W. McCune), volume 7788, pages 189–-228. Springer,
          2013.</li>

        <li>Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley
          Weimer. <a href="pubs/le2011genprog.pdf">GenProg: A Generic Method
            for Automated Software Repair</a>. <b>Transactions on Software
            Engineering (TSE)</b>, 38(1):54–-72, 2012.
            <ul>
                <li>🏅<em>IEEE TSE 50th Anniversary Retrospective Most Influential Paper Award</em></li>
            </ul>
        </li>

        <li>ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie
          Forrest. <a href="pubs/nguyen2012using.pdf">Using Dynamic Analysis to
            Discover Polynomial and Array Invariants</a>. <b>International
            Conference on Software Engineering (ICSE)</b>, pages 683–-693. IEEE,
          2012.
          <ul>
            <li>🏅<em>ACM SIGSOFT Distinguished Paper Award</em></li>
          </ul>
        </li>
        <li>Westley Weimer, Stephanie Forrest, Claire Le Goues, and ThanhVu
          Nguyen. <a href="pubs/weimer2010automatic.pdf">Automatic Program
            Repair with Evolutionary Computation</a>. <b>Communications of the
            ACM (CACM)</b>, 53(5):109–-116, 2010.<br>
          <ul>
            <li>🏅<em>Research Highlight</em></li>
          </ul>
        </li>
        <li>Thang Bui, ThanhVu Nguyen, and Joseph Rizzo. <a href="pubs/bui2009parallel.pdf">Parallel Shared
            Memory
            Strategies For
            Ant-based Optimization Algorithms</a>. <b>Conference on Genetic and
            Evolutionary Computation (GECCO)</b>, pages 1–8. ACM, 2009.
          <ul>
            <li>🏅<em>Best Paper Award</em></li>
          </ul>
        </li>
        <li>Stephanie Forrest, Westley Weimer, ThanhVu Nguyen, and Claire Le
          Goues. <a href="pubs/forrest2009genetic.pdf">A Genetic Programming
            Approach to Automated Software Repair</a>. <b>Conference on Genetic
            and Evolutionary Computation (GECCO)</b>, pages 947-–954. ACM,
          2009.
          <ul>
            <li>🏅<em>Best Paper Award</em></li>
            <li>🏅<em>ACM SIGEVO 10-year Impact Award</em></li>
          </ul>
        </li>
        <li>Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie
          Forrest. <a href="pubs/weimer2009automatically.pdf">Automatically
            Finding Patches Using Genetic Programming</a>. <b>International
            Conference on Software Engineering (ICSE)</b>, pages 364-–367. IEEE,
          2009.
          <ul>
            <li>🏅<em>ACM SIGSOFT Distinguished Paper Award</em></li>
            <li>🏅<em>Manfred Paul Award for ExcellenceSoftware: Theory and
                Practice</em></li>
            <li>🏅<em>ACM SIGSOFT 10-year Most Influential Paper Award</em></li>
          </ul>
        </li>
        <li>ThanhVu Nguyen, Westley Weimer, Claire Le Goues, and Stephanie
          Forrest. <a href="pubs/nguyen2009using.pdf">Using Execution Paths to
            Evolve Software Patches</a>. International Conference on Software
          Testing, Verification and Validation Workshops (ICST), pages 152-–153.
          IEEE, 2009.
          <ul>
            <li>🏅<em>Best Short Paper Award and Best Presentation Award</em></li>
          </ul>
        </li>
        <li>Thang Bui, ThanhVu Nguyen, Chirag Patel, and Kim-Anh Phan.
          <a href="pubs/bui2008ant.pdf"> An Ant-based Algorithm for Coloring Graphs</a>.
          Discrete Applied Mathematics, 156(2):190-–200, 2008.</li>

        <li>James Smith, III and ThanhVu Nguyen.
          <a href="pubs/smith2007fuzzy.pdf">Fuzzy Decision Trees for
            Planning and Autonomous Control of a Coordinated Team of UAVs</a>.
          International Society for Optical Engineering. SPIE, May 2007.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2007autonomous.pdf">Autonomous and
            Cooperative
            Robotic Behavior Based on Fuzzy Logic and Genetic Programming</a>.
          Integrated Computer-Aided Engineering, 14(2):141-–159, 2007.</li>
        <li>James Smith, III and ThanhVu Nguyen.
          <a href="pubs/smith2007genetic.pdf">Genetic Program based Data Mining
            of Fuzzy Decision Trees and Methods of Improving Convergence and
            Reducing Bloat</a>.
          International Society for Optical Engineering. SPIE,
          2007.</li>
        <li>G Viamontes, M Amduka, J Russo, Craven M, and T Nguyen. <a
                                                                      href="pubs/viamontes2007efficient.pdf">Efficient
            Memoization
            Strategies for Object Recognition with a Multi-Core Architecture</a>.
          Annual High Performance Embedded Computing Workshop (HPEC). IEEE,
          2007.
          <ul>
            <li>🏅<em>Outstanding Submission</em></li>
          </ul>
        </li>
        <li>Thang Bui and ThanhVu Nguyen. <a href="pubs/bui2006agent.pdf">An Agent-based Algorithm for
            Generalized
            Graph Colorings</a>. <b>Conference on Genetic and Evolutionary
            Computation (GECCO)</b>, pages 19–-26. ACM, 2006.
          <ul>
            <li>Erdos number: 4 (through Thang N. Bui)</li>
          </ul>
        </li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006genetic.pdf">Genetic Program based Data
            Mining to
            Reverse Engineer Digital Logic</a>. International Society for Optical
          Engineering, pages 24-–35. SPIE, 2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006resource.pdf">Resource Manager for an
            Autonomous
            Coordinated Team of UAVs</a>. International Society for Optical
          Engineering, pages 118-–129. SPIE, 2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006creating.pdf">Creating Fuzzy Decision
            Algorithms
            Using Genetic Program Based Data Mining Program</a>. Annual Meeting of
          the North American Fuzzy Information Processing Society (NAFIPS), pages
          471-–477. IEEE, 2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006fuzzy.pdf">Fuzzy Logic Based Resource
            Manager for
            a Team of UAVs</a>. Annual Meeting of the North American Fuzzy
          Information Processing Society (NAFIPS), pages 463–-470. IEEE,
          2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006fuzzy2.pdf">Fuzzy Logic Based UAV
            Allocation and
            Coordination</a>. International Conference on Informatics in Control
          Automation and Robotics (ICINCO), pages 81-–94. Springer, 2006.
          <ul>
            <li>🏅<em>Best Paper Award</em></li>
          </ul>
        </li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006evolutionary.pdf">Evolutionary Data
            Mining
            Approach to Creating Digital Logic</a>. International Conference on
          Informatics in Control Automation and Robotics (ICINCO), pages 107-–113.
          Springer, 2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2006guiding.pdf">Guiding Genetic Program
            Based Data
            Mining Using Fuzzy Rules</a>. Intelligent Data Engineering and Automated
          Learning (IDEAL), pages 1337–-1345. Springer, 2006.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2005data.pdf">Data Mining based Automated
            Reverse
            Engineering and Defect Discovery</a>. International Society for Optical
          Engineering, pages 232–-242. SPIE, 2005.</li>
        <li>James Smith, III and ThanhVu Nguyen. <a href="pubs/smith2005distributed.pdf">Distributed Autonomous
            Systems:
            Resource Management, Planning, and Control Algorithms</a>. International
          Society for Optical Engineering, pages 65–-76. SPIE, 2005.</li>
      </ol>
    </div>

    <h3 id="disserations">Dissertations</h3>
    <div class="myborder">
      <ol>
        <li>Guolong Zheng.
          Ensure Correctness for Imperative and Declarative Programs.
          Ph.D. thesis, University of Nebraska-Lincoln, May 2022.</li>
        <li>ThanhVu Nguyen.
          <a href="pubs/nguyen2014automating.pdf">Automating Program Verification
            and Repair Using Invariant Analysis and Test-input Generation</a>.
          Ph.D. thesis, University of New Mexico, August 2014.</li>
        <li>ThanhVu Nguyen. <a href="pubs/nguyen2006graph.pdf">On the
            Graph Coloring Problem and Its Generalizations</a>.
          Master's thesis, The Pennsylvania State University, December 2006.</li>
      </ol>
    </div>

    <hr>

    <h2 id="links">Roars Links</h2>
    <div class="myborder">
      <ul>
        <li>Git repos: <a href="https://git.roars.dev">git.roars.dev</a></li>
        <li>Google Scholar: <a href="https://scholars.roars.dev">scholars.roars.dev</a></li>
        <li>Photos: <a href="https://photos.roars.dev">photos.roars.dev</a></li>
        <li>Wiki: <a href="https://wiki.roars.dev">wiki.roars.dev</a></li>
      </ul>

    <hr>

    <h2 id="acknowledgement">Acknowledgement</h2>
    Our work has been generously supported by NSF, Army Research Office, Amazon, Facebook, UNL, and GMU. <b>Thank you</b>!


    <hr>

    <h2 id="contact">Contact</h2>
    <address>
      George Mason University<br>
      Nguyen Engineering Building #4430<br>
      4400 University Drive<br>
      Fairfax, VA 22030<br>
      📬 &nbsp;Email: <b>info at roars dot dev</b>
    </address>
    <hr>

    <!-- <footer> -->
      <!--   <p style="text-align:right">Last updated: <b>April 2023</b></p> -->
      <!-- </footer> -->

    <script>
        console.log("ROARS msg: Hello from ROARS!");
    </script>

</body>
</html>