TY - GEN
T1 - Learning universally quantified invariants of linear data structures
AU - Garg, Pranav
AU - Löding, Christof
AU - Madhusudan, P.
AU - Neider, Daniel
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84881182290&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84881182290&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39799-8_57
DO - 10.1007/978-3-642-39799-8_57
M3 - Conference contribution
AN - SCOPUS:84881182290
SN - 9783642397981
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 813
EP - 829
BT - Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings
T2 - 25th International Conference on Computer Aided Verification, CAV 2013
Y2 - 13 July 2013 through 19 July 2013
ER -