ICE: A Robust Framework for Learning Invariants

Abstract. We introduce ICE, a robust learning paradigm for synthesizing invari-ants, 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 interpre-tation 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 algo-rithms in a verification tool and show they are robust, practical, and efficient.