Learning the Boundary of Inductive Invariants

TL;DR

This paper introduces the fence condition, a geometric property of invariants, enabling polynomial-time inference of certain invariants using concept learning techniques and SAT solvers, with analysis of transformation robustness.

Contribution

It establishes the first polynomial complexity result for an invariant inference algorithm based on the fence condition and extends invariant inference to broader classes using concept learning.

Findings

Polynomial-time inference for monotone DNF invariants.

Extension to larger invariant classes via concept learning.

Fence condition's sensitivity to program transformations.

Abstract

We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning to answer open problems in invariant inference theory. The condition requires the invariant's boundary---the states whose Hamming distance from the invariant is one---to be backwards reachable from the bad states in a small number of steps. Using this condition, we obtain the first polynomial complexity result for an interpolation-based invariant inference algorithm, efficiently inferring monotone DNF invariants with access to a SAT solver as an oracle. We further harness Bshouty's seminal result in concept learning to efficiently infer invariants of a larger syntactic class of invariants beyond monotone DNF. Lastly, we consider the robustness of inference under program transformations. We show that some simple transformations preserve the fence condition, and that it is sensitive to more complex transformations.