ThanhVu (Vũ) H. Nguyen

me.png 

Assistant Professor
Department of Computer Science & Engineering 
364 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).

CV

Teaching

  • Foundation of Software Engineering (SOFT 260): Fall 2018
  • Software Verification (CSCE 990): Fall 2017, Fall 2016
  • Automata, Computation and Formal Languages (CSCE 428/828): Spring 2018, Spring 2017

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, determine program complexities, and synthesize program repairs.

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?

Services

2019

  • FSE: Program Committee
  • ICSE: Program Committee (Demo Track)

2018

Projects

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

  • DIG: a hybrid dynamic and static tool that generates polynomial invariants for C and Java programs. DIG uses a counterexample-guided algorithm to compute candidate invariants and statically checks inferred invariants.
  • DIG (original): 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