DIG: A Framework for Inferring Numerical Program Invariants


ThanhVu Nguyen

Event Details
Thursday, September 28, 2017
Talk:
4–5 p.m., Avery 115

Reception:
3:30 p.m., Avery 348

ThanhVu Nguyen, Ph.D.

Assistant Professor, Department of Computer Science and Engineering, University of Nebraska–Lincoln

Abstract

Software bugs are a persistent feature of daily life—crashing web browsers, allowing cyberattacks, and distorting the results of scientific computations. One approach to improving software uses program invariants— mathematical descriptions of program behaviors—to verify code and detect bugs. Current invariant generation techniques lack support for complex yet important forms of invariants, such as general polynomial relations over numerical variables. This talk presents DIG, an iterative algorithm that combines static and dynamic analyses for discovering useful numerical program invariants. We describe theoretical and empirical results showing that DIG can efficiently and accurately find many important invariants in real-world uses, e.g., nonlinear polynomial properties in complex programs.

Speaker Bio

ThanhVu Nguyen received BS and MS degrees in computer science from Penn State University and a PhD in computer science at the University of New Mexico. After graduate school, he did a postdoc at the University of Maryland, College Park. Currently, he is an assistant professor in computer science at the University of Nebraska, Lincoln.  His research focuses on using static and dynamic analyses for automatic invariant generation and program repair.