Files in this item



application/pdfmain.pdf (318kB)
Main article - Updated 2014/02/10PDF


Title:ICE: A Robust Learning Framework for Synthesizing Invariants
Author(s):Garg, Pranav; Loding, Christof; Madhusudan, P.; Neider, Daniel
Subject(s):Program Verification
Invariant Synthesis
Abstract:We introduce a new paradigm for using black-box learning to synthesize invariants called ICE-learning that learns using examples, counter-examples, and implications, and show that it allows building honest teachers and convergent mechanisms for invariant synthesis. We observe that existing algorithms for black-box abstract interpretation can be interpreted as monotonic ICE learning algorithms, develop two classes of new non-monotonic ICE-learning domains, one for learning numerical invariants for scalar variables and one for quantified invariants for arrays and dynamic lists, and establish convergence results for them. We implement these ICE learning algorithms in a prototype verifier and show that the robustness that it brings is practical and effective.
Issue Date:2013-10
Genre:Technical Report
Date Available in IDEALS:2013-11-07

This item appears in the following Collection(s)

Item Statistics