{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/106251"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/106251","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Learning frameworks for program synthesis","abstract":"The field of synthesis is seeing a renaissance in recent years, where the task is to automatically synthesize small expressions or programs. One of the most prominent techniques counterexample guided inductive synthesis (CEGIS), uses a teacher(verification oracle) and a learner(learning algorithm) to learn such expressions across multiple rounds. A learning framework is a sub-framework of CEGIS where the learner is entirely agnostic of the specification and learns only from input-output examples provided by the teacher as natural notions of counterexamples. Thus, learning frameworks for synthesis have three components: the verification oracle, the notion of a natural counterexample, and the learning algorithm. The goals of this thesis are to study learning frameworks for synthesis, developing new and more efficient algorithms for learning, exploring new classes of counterexamples, and finding applications of synthesis to new domains. Specifically, by co-designing the notion of counterexamples, the learning algorithms, the verification oracle, and taking into account the aspects of the application domain, we achieved more effective program synthesis. We discuss learning frameworks for four different applications, illustrating the co-design of oracle-counterexample-learner for each of them. For the first application, we developed a general purpose SyGuS solver for piece-wise functions, using multiple learners to learn parts of the expression modularly and then compose them together to get the final expression. Second, we considered the application of automatic verification, where we synthesized inductive invariants using incomplete verification oracles. We also propose a novel property driven ICE learning algorithm to learn conjunctive inductive invariants. We considered specification mining for the next two applications, where we learned preconditions and postconditions of a method. Instead of using a verification engine as the oracle, which is not efficient, does not scale, and needs loop invariants, we bypassed all these limitations by using a test generator as the oracle.","abstract_html":"The field of synthesis is seeing a renaissance in recent years, where the task is to automatically synthesize small expressions or programs. One of the most prominent techniques counterexample guided inductive synthesis (CEGIS), uses a teacher(verification oracle) and a learner(learning algorithm) to learn such expressions across multiple rounds. A learning framework is a sub-framework of CEGIS where the learner is entirely agnostic of the specification and learns only from input-output examples provided by the teacher as natural notions of counterexamples. Thus, learning frameworks for synthesis have three components: the verification oracle, the notion of a natural counterexample, and the learning algorithm. The goals of this thesis are to study learning frameworks for synthesis, developing new and more efficient algorithms for learning, exploring new classes of counterexamples, and finding applications of synthesis to new domains. Specifically, by co-designing the notion of counterexamples, the learning algorithms, the verification oracle, and taking into account the aspects of the application domain, we achieved more effective program synthesis. We discuss learning frameworks for four different applications, illustrating the co-design of oracle-counterexample-learner for each of them. For the first application, we developed a general purpose SyGuS solver for piece-wise functions, using multiple learners to learn parts of the expression modularly and then compose them together to get the final expression. Second, we considered the application of automatic verification, where we synthesized inductive invariants using incomplete verification oracles. We also propose a novel property driven ICE learning algorithm to learn conjunctive inductive invariants. We considered specification mining for the next two applications, where we learned preconditions and postconditions of a method. Instead of using a verification engine as the oracle, which is not efficient, does not scale, and needs loop invariants, we bypassed all these limitations by using a test generator as the oracle.","abstract_has_math":false,"creators":["Saha, Shambwaditya"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Parthasarathy, Madhusudan","Viswanathan, Mahesh","Xie, Tao","Singh, Rishabh"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-12","date_published":"2019-12","updated_at":"2026-07-22T22:24:45Z","subjects":["program synthesis","machine learning","program verification"],"languages":["en"],"rights":["Copyright 2019 Shambwaditya Saha"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/106251","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan","Viswanathan, Mahesh","Xie, Tao","Singh, Rishabh"]},{"key":"dc:creator","label":"Author","values":["Saha, Shambwaditya"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-12","2020-03-02T21:58:26Z","2019-12-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["program synthesis","machine learning","program verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Shambwaditya Saha"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/106251"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The field of synthesis is seeing a renaissance in recent years, where the task is to automatically synthesize small expressions or programs. One of the most prominent techniques counterexample guided inductive synthesis (CEGIS), uses a teacher(verification oracle) and a learner(learning algorithm) to learn such expressions across multiple rounds. A learning framework is a sub-framework of CEGIS where the learner is entirely agnostic of the specification and learns only from input-output examples provided by the teacher as natural notions of counterexamples. Thus, learning frameworks for synthesis have three components: the verification oracle, the notion of a natural counterexample, and the learning algorithm. The goals of this thesis are to study learning frameworks for synthesis, developing new and more efficient algorithms for learning, exploring new classes of counterexamples, and finding applications of synthesis to new domains. Specifically, by co-designing the notion of counterexamples, the learning algorithms, the verification oracle, and taking into account the aspects of the application domain, we achieved more effective program synthesis. We discuss learning frameworks for four different applications, illustrating the co-design of oracle-counterexample-learner for each of them. For the first application, we developed a general purpose SyGuS solver for piece-wise functions, using multiple learners to learn parts of the expression modularly and then compose them together to get the final expression. Second, we considered the application of automatic verification, where we synthesized inductive invariants using incomplete verification oracles. We also propose a novel property driven ICE learning algorithm to learn conjunctive inductive invariants. We considered specification mining for the next two applications, where we learned preconditions and postconditions of a method. Instead of using a verification engine as the oracle, which is not efficient, does not scale, and needs loop invariants, we bypassed all these limitations by using a test generator as the oracle.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-02-28 without embargo terms","The student, Shambwaditya Saha, accepted the attached license on 2019-12-05 at 11:59.","The student, Shambwaditya Saha, submitted this Dissertation for approval on 2019-12-05 at 12:11.","This Dissertation was approved for publication on 2019-12-05 at 14:59.","DSpace SAF Submission Ingestion Package generated from Vireo submission #14715 on 2020-02-28 at 17:15:48","Made available in DSpace on 2020-03-02T21:58:26Z (GMT). No. of bitstreams: 2 SAHA-DISSERTATION-2019.pdf: 1495572 bytes, checksum: 7e13242e1b11bdb6ba92dfddae94e6c1 (MD5) LICENSE.txt: 4214 bytes, checksum: b9dbe711a59c3c56e99130a07bba6dcd (MD5) Previous issue date: 2019-12-05"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Learning frameworks for program synthesis"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan","Viswanathan, Mahesh","Xie, Tao","Singh, Rishabh"],"dc:creator":["Saha, Shambwaditya"],"dc:date":["2019-12","2020-03-02T21:58:26Z","2019-12-05"],"dc:description":["The field of synthesis is seeing a renaissance in recent years, where the task is to automatically synthesize small expressions or programs. One of the most prominent techniques counterexample guided inductive synthesis (CEGIS), uses a teacher(verification oracle) and a learner(learning algorithm) to learn such expressions across multiple rounds. A learning framework is a sub-framework of CEGIS where the learner is entirely agnostic of the specification and learns only from input-output examples provided by the teacher as natural notions of counterexamples. Thus, learning frameworks for synthesis have three components: the verification oracle, the notion of a natural counterexample, and the learning algorithm. The goals of this thesis are to study learning frameworks for synthesis, developing new and more efficient algorithms for learning, exploring new classes of counterexamples, and finding applications of synthesis to new domains. Specifically, by co-designing the notion of counterexamples, the learning algorithms, the verification oracle, and taking into account the aspects of the application domain, we achieved more effective program synthesis. We discuss learning frameworks for four different applications, illustrating the co-design of oracle-counterexample-learner for each of them. For the first application, we developed a general purpose SyGuS solver for piece-wise functions, using multiple learners to learn parts of the expression modularly and then compose them together to get the final expression. Second, we considered the application of automatic verification, where we synthesized inductive invariants using incomplete verification oracles. We also propose a novel property driven ICE learning algorithm to learn conjunctive inductive invariants. We considered specification mining for the next two applications, where we learned preconditions and postconditions of a method. Instead of using a verification engine as the oracle, which is not efficient, does not scale, and needs loop invariants, we bypassed all these limitations by using a test generator as the oracle.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-02-28 without embargo terms","The student, Shambwaditya Saha, accepted the attached license on 2019-12-05 at 11:59.","The student, Shambwaditya Saha, submitted this Dissertation for approval on 2019-12-05 at 12:11.","This Dissertation was approved for publication on 2019-12-05 at 14:59.","DSpace SAF Submission Ingestion Package generated from Vireo submission #14715 on 2020-02-28 at 17:15:48","Made available in DSpace on 2020-03-02T21:58:26Z (GMT). No. of bitstreams: 2 SAHA-DISSERTATION-2019.pdf: 1495572 bytes, checksum: 7e13242e1b11bdb6ba92dfddae94e6c1 (MD5) LICENSE.txt: 4214 bytes, checksum: b9dbe711a59c3c56e99130a07bba6dcd (MD5) Previous issue date: 2019-12-05"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/106251"],"dc:language":["en"],"dc:rights":["Copyright 2019 Shambwaditya Saha"],"dc:subject":["program synthesis","machine learning","program verification"],"dc:title":["Learning frameworks for program synthesis"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:45Z"}