Files in this item



application/pdfSURESHKUMAR-THESIS-2021.pdf (688kB)
(no description provided)PDF


Title:Learning inductive invariants using Winnow algorithm
Author(s):Suresh Kumar, Anjana
Advisor(s):Parthasarathy, Madhusudan
Department / Program:Electrical & Computer Eng
Discipline:Electrical & Computer Engr
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Invariant Synthesis
Machine Learning
Horn-ICE Learning
Conjunctive Formulas
Abstract:Invariant synthesis is crucial for program verification and is a challenging task. We present a new concrete learning algorithm, Winnow-ICE, to synthesize inductive invariants for proving that a program is correct by validating its assertions. Winnow is an online learning algorithm that can be used to learn Boolean formulae from positive, negative and implication counterexamples. We implemented the Winnow algorithm as a plug-in for the Horn-ICE framework which is built on the Boogie program verifier. We compare our learning algorithm against Houdini and Sorcar by evaluating the algorithm on a subset of two different classes of benchmarks. The first class of benchmark is obtained from the GPUVerify tool, and the second class of benchmark is derived from Neider et al. (2018). On the GPUVerify benchmark suite, it is noted that the Winnow algorithm takes considerably fewer rounds as compared to Sorcar for similar total performance in time, whereas, as compared to the Houdini, the total time taken is notably large for a similar performance in total number of rounds. On the Dryad benchmark suite, it is observed that the Winnow algorithm takes fewer rounds as compared to Houdini and more rounds as compared to Sorcar; however, the Winnow algorithm is slower in comparison to both Sorcar and Houdini.
Issue Date:2021-04-26
Rights Information:Copyright 2021 Anjana Suresh Kumar
Date Available in IDEALS:2021-09-17
Date Deposited:2021-05

This item appears in the following Collection(s)

Item Statistics