DIG: A Framework for Inferring Numerical Program Invariants
Thursday, September 28, 2017
4–5 p.m., Avery 115
3:30 p.m., Avery 348
ThanhVu Nguyen, Ph.D.Assistant Professor, Department of Computer Science and Engineering, University of Nebraska–Lincoln
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.
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.