Learning inductive invariants using Winnow algorithm

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.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2021

Author dc:creator

• Suresh Kumar, Anjana

Contributors dc:contributor

• Parthasarathy, Madhusudan

• Invariant Synthesis
• Machine Learning
• Horn-ICE Learning
• Winnow
• Conjunctive Formulas

Statement dc:rights

• Copyright 2021 Anjana Suresh Kumar

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/110545