ThanhVu (Vũ) H. Nguyen


Assistant Professor
Department of Computer Science & Engineering 
256 Avery Hall 
University of Nebraska-Lincoln 
Lincoln, NE 68588-0115 

Office: 359 Avery Hall, Tel: 402-472-5086, Email: tnguyen at

I am an assistant professor in the CSE department at UNL and a member of the E2 software engineering lab. I work in the areas of Software Engineering and Programming Languages to improve software quality. I am interested in answering questions such as

In particular, my research uses dynamic and static techniques to discover program invariants, prove program correctness, and synthesize program repairs. Previously, I also worked with nature-inspired techniques such as evolutionary computing and ant-based algorithms.

Opportunities: I am always looking for new students at both graduate and undergraduate levels to work with me on SE and PL projects! Successfull candidates should have strong programming skills and solid knowledge in core computer science (e.g., data structures and algorithms).



Work Experience


  • Fall 2016 : CSCE 990 Software Verification


wordle.png My research interests lie in the intersection of software engineering and programming languages, with a particular focus on using static and dynamic analyses to verify and repair programs.

  • Invariant generation using static and dynamic analyses
  • Program verification using theorem proving
  • Program synthesis using constraint solving


Links to my research projects, see publications for technical details.

  • iGen: dynamic interaction generator that finds boolean expressions over configurable options.
  • DIG: a dynamic invariant generator that supports (nonlinear) polynomial, disjunctive relations, and array invariants. This project also includes KTP, a theorem prover using k-induction and SMT solver.
  • CETI: (correcting errors using test-input), automatic program repair using test input generation.
  • GenProg: an evolutionary approach to automatic program repair.
  • Coloring: an ant-based algorithm for the graph coloring problem and its generalizations bandwidth coloring, multi coloring, and bandwidth multi coloring.
  • MaxClique: an ant-based algorithm to find a maximum clique from a given graph. It can be used with a compiler that supports OpenMP (e.g., GCC or Intel) for parallelism.
  • Dimacs's Clique and Graph Color instances: these benchmark graphs were collected and archived during my Master thesis.