{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/127256"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/127256","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Towards eliminating expert creative help in automated reasoning","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","abstract_has_math":false,"creators":["Murali, Adithya"],"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","Singh, Gagandeep","Jhala, Ranjit","Chaudhuri, Swarat"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-12-03","date_published":"2024-12-03","updated_at":"2026-07-22T22:25:03Z","subjects":["Automated Verification","Automated Reasoning","Logic","Creativity Gaps","Logic Learning","Formula Synthesis","Learning For Bridging Creativity Gaps","Data-driven Logic Learning","Democratizing Verification","First-order Logic With Recursive Definitions","First-order Logic With Least Fixpoints","Completeness","Functional Programs","Refinement Types","Inductive Lemma Synthesis","Model-guided Synthesis","Verification Language Design","Predictable Verification","Axiom Synthesis","Axiom Discovery","Axiom Learning","Programming Languages","Verification","Smt Solvers"],"languages":["en","eng"],"rights":["Copyright 2024 Adithya Murali"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/127256","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan","Viswanathan, Mahesh","Singh, Gagandeep","Jhala, Ranjit","Chaudhuri, Swarat"]},{"key":"dc:creator","label":"Author","values":["Murali, Adithya"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-12-03","2024-12"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"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":["Automated Verification","Automated Reasoning","Logic","Creativity Gaps","Logic Learning","Formula Synthesis","Learning For Bridging Creativity Gaps","Data-driven Logic Learning","Democratizing Verification","First-order Logic With Recursive Definitions","First-order Logic With Least Fixpoints","Completeness","Functional Programs","Refinement Types","Inductive Lemma Synthesis","Model-guided Synthesis","Verification Language Design","Predictable Verification","Axiom Synthesis","Axiom Discovery","Axiom Learning","Programming Languages","Verification","Smt Solvers"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2024 Adithya Murali"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/127256"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Adithya Murali, accepted the attached license on 2024-12-02 at 21:02.","The student, Adithya Murali, submitted this Dissertation for approval on 2024-12-02 at 21:22.","This Dissertation was approved for publication on 2024-12-03 at 14:32.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21459 on 2025-03-28 at 14:27:53","The democratization of automated reasoning is a dream for computer scientists like few others. However, despite many years of progress there continue to exist fundamental obstacles in the way. In this thesis we identify one of the key obstacles: the inescapable need for expert help encountered when using automated reasoning tools or algorithms to prove rich sets of properties. This help takes many forms across the many reasoning frameworks that exist, but we argue that in many widely used frameworks the help is a technical intervention that experts are able to come up with by studying a problem, simply using their experience and creativity. In this work we seek to unravel the nature of this creative technical help and take steps towards eliminating it. Although at first sight the workflow we describe may appear informal or unorganized, our study reveals that it is possible to formally characterize the limits of the reasoning power of various automatic tools and heuristics. Furthermore, we show that the expert help in fact bridges (again in a formal sense) the gap between the limits of the reasoning algorithms and the power needed to prove the properties desired. We dub such gaps in automated reasoning creativity gaps and develop new theoretical tools to formally characterize them. Understanding the role of the expert help in a formal sense allows us to formulate well-defined computational problems to solve in order to bridge creativity gaps. We argue that such problems can be solved effectively using a form of learning we call logic learning in this thesis, which refers to the problem of learning logical formulas from rich example structures/ logical models. We develop new frameworks and algorithms for logic learning and use them to bridge different creativity gaps. In a third part of our work, we apply the lens of thinking about the dynamics between expert help and automation to interrogate design principles for new verification paradigms that can minimize the kind of user frustrations we focus on in this work, namely dealing with the opaqueness of creativity gaps and the inability to provide the required help to bridge the gaps without deep verification expertise. We formulate the problem of designing a predictable verification framework and develop a new framework for verifying heap manipulating programs that offers a predictable verification experience. We believe that the contributions of this work take significant steps towards eliminating creativity gaps in automated reasoning, and in doing so pave the way further for progress towards the democratization of automated reasoning."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Towards eliminating expert creative help in automated reasoning"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan","Viswanathan, Mahesh","Singh, Gagandeep","Jhala, Ranjit","Chaudhuri, Swarat"],"dc:creator":["Murali, Adithya"],"dc:date":["2024-12-03","2024-12"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Adithya Murali, accepted the attached license on 2024-12-02 at 21:02.","The student, Adithya Murali, submitted this Dissertation for approval on 2024-12-02 at 21:22.","This Dissertation was approved for publication on 2024-12-03 at 14:32.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21459 on 2025-03-28 at 14:27:53","The democratization of automated reasoning is a dream for computer scientists like few others. However, despite many years of progress there continue to exist fundamental obstacles in the way. In this thesis we identify one of the key obstacles: the inescapable need for expert help encountered when using automated reasoning tools or algorithms to prove rich sets of properties. This help takes many forms across the many reasoning frameworks that exist, but we argue that in many widely used frameworks the help is a technical intervention that experts are able to come up with by studying a problem, simply using their experience and creativity. In this work we seek to unravel the nature of this creative technical help and take steps towards eliminating it. Although at first sight the workflow we describe may appear informal or unorganized, our study reveals that it is possible to formally characterize the limits of the reasoning power of various automatic tools and heuristics. Furthermore, we show that the expert help in fact bridges (again in a formal sense) the gap between the limits of the reasoning algorithms and the power needed to prove the properties desired. We dub such gaps in automated reasoning creativity gaps and develop new theoretical tools to formally characterize them. Understanding the role of the expert help in a formal sense allows us to formulate well-defined computational problems to solve in order to bridge creativity gaps. We argue that such problems can be solved effectively using a form of learning we call logic learning in this thesis, which refers to the problem of learning logical formulas from rich example structures/ logical models. We develop new frameworks and algorithms for logic learning and use them to bridge different creativity gaps. In a third part of our work, we apply the lens of thinking about the dynamics between expert help and automation to interrogate design principles for new verification paradigms that can minimize the kind of user frustrations we focus on in this work, namely dealing with the opaqueness of creativity gaps and the inability to provide the required help to bridge the gaps without deep verification expertise. We formulate the problem of designing a predictable verification framework and develop a new framework for verifying heap manipulating programs that offers a predictable verification experience. We believe that the contributions of this work take significant steps towards eliminating creativity gaps in automated reasoning, and in doing so pave the way further for progress towards the democratization of automated reasoning."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/127256"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Adithya Murali"],"dc:subject":["Automated Verification","Automated Reasoning","Logic","Creativity Gaps","Logic Learning","Formula Synthesis","Learning For Bridging Creativity Gaps","Data-driven Logic Learning","Democratizing Verification","First-order Logic With Recursive Definitions","First-order Logic With Least Fixpoints","Completeness","Functional Programs","Refinement Types","Inductive Lemma Synthesis","Model-guided Synthesis","Verification Language Design","Predictable Verification","Axiom Synthesis","Axiom Discovery","Axiom Learning","Programming Languages","Verification","Smt Solvers"],"dc:title":["Towards eliminating expert creative help in automated reasoning"],"dc:type":["text","Thesis"],"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:25:03Z"}