DIG: A Framework for Inferring Numerical Program Invariants

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.