Learning Invariants using Decision Trees
The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other ML-based invariant inference techniques. In particular, it scales well to large sample sets.
Code (0)
등록된 구현이 없습니다.
Tasks
Binary ClassificationSimilar Papers 제목 키워드 기반
Horn-ICE Learning for Synthesizing Invariants and Contracts
We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns fro…
Invariants for level-1 phylogenetic networks under the Cavendar-Farris-Neyman Model
Phylogenetic networks can model more complicated evolutionary phenomena that trees fail to capture such as horizontal gene transfer and hybridization. The same Markov models that are used to model evolution on trees can …
Verifying Safety of Behaviour Trees in Event-B
Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans …
Decision MakingInvariants for level-1 phylogenetic networks under the random walk 4-state Markov model
Phylogenetic networks can represent evolutionary events that cannot be described by phylogenetic trees, such as hybridization, introgression, and lateral gene transfer. Studying phylogenetic networks under a statistical …
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…