When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic

Zachary Kincaid, Nicolas Koh, Shaowei Zhu

Research output: Contribution to journalArticlepeer-review

3 Scopus citations

Abstract

This paper presents a theory of non-linear integer/real arithmetic and algorithms for reasoning about this theory. The theory can be conceived of as an extension of linear integer/real arithmetic with a weakly-axiomatized multiplication symbol, which retains many of the desirable algorithmic properties of linear arithmetic. In particular, we show that the conjunctive fragment of the theory can be effectively manipulated (analogously to the usual operations on convex polyhedra, the conjunctive fragment of linear arithmetic). As a result, we can solve the following consequence-finding problem: given a ground formula F, find the strongest conjunctive formula that is entailed by F. As an application of consequence-finding, we give a loop invariant generation algorithm that is monotone with respect to the theory and (in a sense) complete. Experiments show that the invariants generated from the consequences are effective for proving safety properties of programs that require non-linear reasoning.

Original languageEnglish (US)
Pages (from-to)1275-1307
Number of pages33
JournalProceedings of the ACM on Programming Languages
Volume7
Issue numberPOPL
DOIs
StatePublished - Jan 9 2023

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Convex polyhedra
  • Decision procedures
  • Nonlinear invariant generation
  • Polynomial ideals
  • Program analysis
  • Theory of arithmetic

Fingerprint

Dive into the research topics of 'When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic'. Together they form a unique fingerprint.

Cite this