Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
ICE: A Robust Framework for Learning Invariants
verfasst von : Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider
Erschienen in: Computer Aided Verification
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We introduce ICE, a robust learning paradigm for synthesizing invariants, that learns using examples, counter-examples, and
implications
, and show that it admits honest teachers and strongly convergent mechanisms for invariant synthesis. We observe that existing algorithms for black-box abstract interpretation can be interpreted as ICE-learning algorithms. We develop new strongly convergent ICE-learning algorithms for two domains, one for learning Boolean combinations of numerical invariants for scalar variables and one for
quantified
invariants for arrays and dynamic lists. We implement these ICE-learning algorithms in a verification tool and show they are robust, practical, and efficient.