DIG: A dynamic invariant generator for polynomial and array invariants

Thanhvu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest

Research output: Contribution to journalArticle

14 Scopus citations

Abstract

This article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both nonlinear equalities and inequalities of arbitrary degree defined over numerical program variables. For array invariants, DIG generates nested relations among multidimensional array variables. These properties are nontrivial and challenging for current static and dynamic invariant analysis methods. The key difference between DIG and existing dynamic methods is its generative technique, which infers invariants directly from traces, instead of using traces to filter out predefined templates. To generate accurate invariants, DIG employs ideas and tools from the mathematical and formal methods domains, including equation solving, polyhedra construction, and theorem proving; for example, DIG represents and reasons about polynomial invariants using geometric shapes. Experimental results on 27 mathematical algorithms and an implementation of AES encryption provide evidence that DIG is effective at generating invariants for these programs.

Original languageEnglish (US)
JournalACM Transactions on Software Engineering and Methodology
Volume23
Issue number4
DOIs
StatePublished - Sep 5 2014

    Fingerprint

Keywords

  • Array invariants
  • Dynamic analysis
  • Geometric invariant inference
  • Invariant generation
  • Nonlinear invariants
  • Program analysis
  • Theorem proving

ASJC Scopus subject areas

  • Software

Cite this