2026-09-20T20:28:44Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/88026 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Parthasarathy, Madhusudan Parthasarathy, Madhusudan Marinov, Darko Viswanathan, Mahesh Gulwani, Sumit McMillan, Kenneth Garg, Pranav 2015-09-29T20:38:20Z 2015-09-29T20:38:20Z 2015-08 2015-07-14 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. Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-09-29 without embargo terms The student, Pranav Garg, accepted the attached license on 2015-07-13 at 10:16. 2015-8 The student, Pranav Garg, submitted this Dissertation for approval on 2015-07-13 at 10:31. This Dissertation was approved for publication on 2015-07-14 at 11:41. DSpace SAF Submission Ingestion Package generated from Vireo submission #8418 on 2015-09-29 at 13:22:39 Made available in DSpace on 2015-09-29T20:38:20Z (GMT). No. of bitstreams: 2 GARG-DISSERTATION-2015.pdf: 2048698 bytes, checksum: f2a9aaeb832ba2aca78a182f4577f2bc (MD5) LICENSE.txt: 4208 bytes, checksum: 6d4b5511fa73374fd27e44f807d4b1d6 (MD5) Previous issue date: 2015-07-14 application/pdf http://hdl.handle.net/2142/88026 en Copyright 2015 Pranav Garg verification invariants invariant synthesis learning machine learning learning invariants using Implication Counter-Examples (ICE) learning model Learning-based inductive invariant synthesis text text Computer Science Computer Science University of Illinois at Urbana-Champaign Dissertation Ph.D.