ICE: A Robust Learning Framework for Synthesizing Invariants

Garg, Pranav; Loding, Christof; Madhusudan, P.; Neider, Daniel

Permalink

https://hdl.handle.net/2142/45973 Copy

Description

Title

ICE: A Robust Learning Framework for Synthesizing Invariants

Author(s)

• Garg, Pranav
• Loding, Christof
• Madhusudan, P.
• Neider, Daniel

Issue Date

2013-10

Keyword(s)

• Program Verification
• Invariant Synthesis
• Learning

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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/45973

Owning Collections