ThanhVu (Vũ) H. Nguyen


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

Office: 261 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. My research foscuses on program verification (invariant generation) and synthesis (automatic program repair).

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



Work Experience



wordle.png My research focuses on program verification and repair. In particular, I use use 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.

My work aims to answer the following questions:

  • invariant/specification/contract discovery: what does this program do? what properties does it have?
  • program verification: does this program run correctly? does it satisfy certain assertions?",
  • program repair/synthesis: how to automatically repair a program? how to synthesize code with respect to some requirements?


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 existing test-input generation tools.
  • GenProg: an evolutionary approach to automatic program repair.and Best Paper awards.
  • 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.