ThanhVu (Vũ) H. Nguyen

me.png

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

Tel: 402-472-5086, Email: tnguyen@cse.unl.edu

I am an assistant professor in the CSE department at UNL and a member of the E2 software engineering lab. My research focuses on program verification (invariant generation) and synthesis (automatic program repair).

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

Information

Teaching

  • Spring 2017 : CSE 428/828 Automata, Computation and Formal Languages
  • Fall 2016 : CSCE 990 Software Verification

Research

wordle.png My research focuses on program verification and repair. In particular, I use use dynamic and static techniques to discover program properties, 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?

Projects

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

  • DIG2 (or NumInv): a hybrid dynamic and static tool that generates polynomial invariants for C programs. DIG2 uses a counterexample-guided algorithm to compute candidate invariants and statically checks inferred invariants using KLEE.
  • 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.
  • iGen: dynamic interaction generator that finds boolean expressions over configurable options.
  • CETI: (correcting errors using test-input), automatic program repair using existing test-input generation tools.
  • 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.

Benchmarks

Miscs