Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
We propose a data-driven algorithm for numerical invariant synthesis and
verification. The algorithm is based on the ICE-DT schema for learning decision
trees from samples of positive and negative states and implications
corresponding to program transitions. The main issue we address is the
discovery of relevant attributes to be used in the learning process of
numerical invariants. We define a method for solving this problem guided by the
data sample. It is based on the construction of a separator that covers
positive states and excludes negative ones, consistent with the implications.
The separator is constructed using an abstract domain representation of convex
sets. The generalization mechanism of the decision tree learning from the
constraints of the separator allows the inference of general invariants,
accurate enough for proving the targeted property. We implemented our algorithm
and showed its efficiency.