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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
A System Parameterization for Direct Data-Driven Estimator Synthesis
This paper introduces a novel parameterization to characterize unknown linear time-invariant systems using noisy data. The presented parameterization describes exactly the set of all systems consistent with the available…
Data-Driven System Level Synthesis
We establish data-driven versions of the System Level Synthesis (SLS) parameterization of achievable closed-loop system responses for a linear-time-invariant system over a finite-horizon. Inspired by recent work in data-…
On Scaling Data-Driven Loop Invariant Inference
Automated synthesis of inductive invariants is an important problem in software verification. Once all the invariants have been specified, software verification reduces to checking of verification conditions. Although st…
Data-Driven Synthesis of Configuration-Constrained Robust Invariant Sets for Linear Parameter-Varying Systems
We present a data-driven method to synthesize robust control invariant (RCI) sets for linear parameter-varying (LPV) systems subject to unknown but bounded disturbances. A finite-length data set consisting of state, inpu…
SchedulingData-driven computation of invariant sets of discrete time-invariant black-box systems
We consider the problem of computing the maximal invariant set of discrete-time black-box nonlinear systems without analytic dynamical models. Under the assumption that the system is asymptotically stable, the maximal in…