DIG: A dynamic invariant generator for polynomial and array invariants

Thanhvu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest

Research output: Contribution to journalArticle

13 Citations (Scopus)

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 - Jan 1 2014
Externally publishedYes

Fingerprint

Polynomials
Theorem proving
Formal methods
Dynamic analysis
Cryptography

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

DIG : A dynamic invariant generator for polynomial and array invariants. / Nguyen, Thanhvu; Kapur, Deepak; Weimer, Westley; Forrest, Stephanie.

In: ACM Transactions on Software Engineering and Methodology, Vol. 23, No. 4, 01.01.2014.

Research output: Contribution to journalArticle

@article{5a70855e84344ae2b1029074e287d978,
title = "DIG: A dynamic invariant generator for polynomial and array invariants",
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.",
keywords = "Array invariants, Dynamic analysis, Geometric invariant inference, Invariant generation, Nonlinear invariants, Program analysis, Theorem proving",
author = "Thanhvu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest",
year = "2014",
month = "1",
day = "1",
doi = "10.1145/2556782",
language = "English (US)",
volume = "23",
journal = "ACM Transactions on Software Engineering and Methodology",
issn = "1049-331X",
publisher = "Association for Computing Machinery (ACM)",
number = "4",

}

TY - JOUR

T1 - DIG

T2 - A dynamic invariant generator for polynomial and array invariants

AU - Nguyen, Thanhvu

AU - Kapur, Deepak

AU - Weimer, Westley

AU - Forrest, Stephanie

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

KW - Array invariants

KW - Dynamic analysis

KW - Geometric invariant inference

KW - Invariant generation

KW - Nonlinear invariants

KW - Program analysis

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=84907021166&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84907021166&partnerID=8YFLogxK

U2 - 10.1145/2556782

DO - 10.1145/2556782

M3 - Article

AN - SCOPUS:84907021166

VL - 23

JO - ACM Transactions on Software Engineering and Methodology

JF - ACM Transactions on Software Engineering and Methodology

SN - 1049-331X

IS - 4

ER -