Files in this item

FilesDescriptionFormat

application/pdf

application/pdfGARG-DISSERTATION-2015.pdf (2MB)
(no description provided)PDF

Description

Title:Learning-based inductive invariant synthesis
Author(s):Garg, Pranav
Director of Research:Parthasarathy, Madhusudan
Doctoral Committee Chair(s):Parthasarathy, Madhusudan
Doctoral Committee Member(s):Marinov, Darko; Viswanathan, Mahesh; Gulwani, Sumit; McMillan, Kenneth
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2015-07-14
Type:Thesis
URI:http://hdl.handle.net/2142/88026
Rights Information:Copyright 2015 Pranav Garg
Date Available in IDEALS:2015-09-29
Date Deposited:August 201


This item appears in the following Collection(s)

Item Statistics