Learning invariants using decision trees and implication counterexamples

8 years 12 days ago

Download web.engr.illinois.edu

Inductive invariants can be robustly synthesized using a learning model where the teacher is a program veriﬁer who instructs the learner through concrete program conﬁgurations, classiﬁed as positive, negative, and implications. We propose the ﬁrst learning algorithms in this model with implication counter-examples that are based on scalable machine learning techniques. In particular, we extend decision tree learning algorithms, building new scalable and heuristic ways to construct small decision trees using statistical measures that account for implication counterexamples. We implement the learners and an appropriate teacher, and show that they are scalable, efﬁcient and convergent in synthesizing adequate inductive invariants in a suite of more than 50 programs, and superior in performance and convergence than existing constraint-solver based learners.

Pranav Garg 0001, Daniel Neider, P. Madhusudan, Da

Real-time Traffic