Learning-based inductive invariant synthesis

Garg, Pranav

Permalink

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

Description

Title

Learning-based inductive invariant synthesis

Author(s)

Garg, Pranav

Issue Date

2015-07-14

Director of Research (if dissertation) or Advisor (if thesis)

Parthasarathy, Madhusudan

Doctoral Committee Chair(s)

Parthasarathy, Madhusudan

Committee Member(s)

• Marinov, Darko
• Viswanathan, Mahesh
• Gulwani, Sumit
• McMillan, Kenneth

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• verification
• invariants
• invariant synthesis
• learning
• machine learning
• learning invariants using Implication Counter-Examples (ICE) learning model

Abstract

The problem of synthesizing adequate inductive invariants to prove a program correct lies at the heart of automated program verification. We investigate, herein, learning approaches to synthesize inductive invariants of sequential programs towards automatically verifying them. To this end, we identify that prior learning approaches were unduly influenced by traditional machine learning models that learned concepts from positive and negative counterexamples. We argue that these models are not robust for invariant synthesis and, consequently, introduce ICE, a robust learning paradigm for synthesizing invariants that learns using positive, negative and implication counterexamples, and show that it admits honest teachers and strongly convergent mechanisms for invariant synthesis. We develop the first learning algorithms in this model with implication counterexamples for two domains, one for learning arbitrary Boolean combinations of numerical invariants over scalar variables and one for quantified invariants of linear data-structures including arrays and dynamic lists. We implement the ICE learners and an appropriate teacher, and show that the resulting invariant synthesis is robust, practical, convergent, and efficient. In order to deductively verify shared-memory concurrent programs, we present a sequentialization result and show that synthesizing rely-guarantee annotations for them can be reduced to invariant synthesis for sequential programs. Further, for verifying asynchronous event-driven systems, we develop a new invariant synthesis technique that constructs almost-synchronous invariants over concrete system configurations. These invariants, for most systems, are finitely representable, and can be thereby constructed, including for the USB driver that ships with Microsoft Windows phone.

Graduation Semester

2015-8

Type of Resource

text

Permalink

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

Copyright and License Information

Copyright 2015 Pranav Garg

Owning Collections