Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis

John Cyphert, Zachary Kincaid

Research output: Contribution to journalArticlepeer-review

Abstract

This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to generate all polynomial invariants for a restricted class of programs, but cannot be applied to programs outside of this class - -for instance, programs with nested loops, conditional branching, unstructured control flow, etc. There currently lacks approaches to apply these prior methods to the case of general programs. This paper bridges that gap. Instead of restricting the kinds of programs we can handle, our method abstracts every loop into a model that can be solved with prior techniques, bringing to bear prior work on solvable polynomial maps to general programs. While no method can generate all polynomial invariants for arbitrary programs, our method establishes its merit through a monotonicty result. We have implemented our techniques, and tested them on a suite of benchmarks from the literature. Our experiments indicate our techniques show promise on challenging verification tasks requiring non-linear reasoning.

Original languageEnglish (US)
Pages (from-to)724-752
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume8
DOIs
StatePublished - Jan 5 2024

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Algebraic program analysis
  • monotone program analysis
  • polynomial invariants

Fingerprint

Dive into the research topics of 'Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis'. Together they form a unique fingerprint.

Cite this