2014 | OriginalPaper | Chapter
ICE: A Robust Framework for Learning Invariants
Authors : Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider
Published in: Computer Aided Verification
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.