Learning Universally Quantified Invariants of Linear Data Structures
This work addresses the challenge of automated invariant inference for program verification, representing an incremental advance in formal methods.
The paper tackles the problem of learning universally quantified invariants for linear data structures by proposing a new automaton model called quantified data automata (QDAs) and developing polynomial-time active learning algorithms for them, with an application showing efficient learning from dynamic program runs.
We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.