Porous Invariants

TL;DR

This paper introduces porous invariants for affine loops over integers, enabling automatic synthesis and analysis of reachability despite their non-convex, hole-containing nature.

Contribution

It presents the concept of porous invariants, a novel approach for analyzing nondeterministic affine loops with non-convex invariants that can contain holes.

Findings

Porous invariants can be automatically synthesized.

They are effective for reachability analysis in affine loops.

Applicable to various classes of affine loops and target sets.

Abstract

We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets.