Learning inductive invariants using Winnow algorithm
Suresh Kumar, Anjana
Loading…
Permalink
https://hdl.handle.net/2142/110545
Description
Title
Learning inductive invariants using Winnow algorithm
Author(s)
Suresh Kumar, Anjana
Issue Date
2021-04-26
Director of Research (if dissertation) or Advisor (if thesis)
Parthasarathy, Madhusudan
Department of Study
Electrical & Computer Eng
Discipline
Electrical & Computer Engr
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Keyword(s)
Invariant Synthesis
Machine Learning
Horn-ICE Learning
Winnow
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
