Non-linear reasoning for invariant synthesis

Zachary Kincaid, John Cyphert, Jason Breck, Thomas Reps

Research output: Contribution to journalArticlepeer-review

26 Scopus citations

Abstract

Automatic generation of non-linear loop invariants is a long-standing challenge in program analysis, with many applications. For instance, reasoning about exponentials provides a way to find invariants of digital-filter programs, and reasoning about polynomials and/or logarithms is needed for establishing invariants that describe the time or memory usage of many well-known algorithms. An appealing approach to this challenge is to exploit the powerful recurrence-solving techniques that have been developed in the field of computer algebra, which can compute exact characterizations of non-linear repetitive behavior. However, there is a gap between the capabilities of recurrence solvers and the needs of program analysis: (1) loop bodies are not merely systems of recurrence relations-they may contain conditional branches, nested loops, non-deterministic assignments, etc., and (2) a client program analyzer must be able to reason about the closed-form solutions produced by a recurrence solver (e.g., to prove assertions). This paper presents a method for generating non-linear invariants of general loops based on analyzing recurrence relations. The key components are an abstract domain for reasoning about non-linear arithmetic, a semantics-based method for extracting recurrence relations from loop bodies, and a recurrence solver that avoids closed forms that involve complex or irrational numbers. Our technique has been implemented in a program analyzer that can analyze general loops and mutually recursive procedures. Our experiments show that our technique shows promise for non-linear assertion-checking and resource-bound generation.

Original languageEnglish (US)
Article number54
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberPOPL
DOIs
StatePublished - Jan 2018

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Invariant generation
  • Operational calculus
  • Recurrence relation

Fingerprint

Dive into the research topics of 'Non-linear reasoning for invariant synthesis'. Together they form a unique fingerprint.

Cite this