Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes

TL;DR

This paper introduces a data-driven algorithm for synthesizing numerical invariants by automatically generating relevant attributes using decision trees and convex set representations, improving verification accuracy.

Contribution

It presents a novel method for automatic attribute generation guided by data samples, enhancing the effectiveness of numerical invariant synthesis and verification.

Findings

Efficient implementation demonstrating practical applicability.

Effective attribute generation improves invariant accuracy.

Successful verification of targeted properties.

Abstract

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.