{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/127261"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/127261","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Static analysis of differentiable programs","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":["Laurel, Jacob Scott"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Misailovic, Sasa","Singh, Gagandeep","Marinov, Darko","Hückelheim, Jan"],"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":["Static Analysis","Differentiable Programming","Automatic Differentiation","Abstract Interpretation","Programming Languages"],"languages":["en","eng"],"rights":["Copyright 2024 Jacob Scott Laurel"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/127261","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Misailovic, Sasa","Singh, Gagandeep","Marinov, Darko","Hückelheim, Jan"]},{"key":"dc:creator","label":"Author","values":["Laurel, Jacob Scott"]}]},{"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":["Static Analysis","Differentiable Programming","Automatic Differentiation","Abstract Interpretation","Programming Languages"]}]},{"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 Jacob Scott Laurel"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/127261"]}]},{"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, Jacob Laurel, accepted the attached license on 2024-12-03 at 11:00.","The student, Jacob Laurel, submitted this Dissertation for approval on 2024-12-03 at 11:39.","This Dissertation was approved for publication on 2024-12-03 at 14:55.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21472 on 2025-03-28 at 14:27:56","Differentiable Programming which includes Automatic Differentiation (AD), serves as the backbone for machine learning and simultaneously pervades many other domains including graphics and scientific computing. Despite AD’s ubiquity, automated formal reasoning about the derivatives AD computes has lagged. The difficulty in developing automated analyses for differentiable programs stems from the fact that these programs use complicated semantics, contain highly nonlinear operations (e.g., the chain rule) and involve thousands of program variables. Thus, developing program analyses for AD that are simultaneously general, precise, and scalable remains a challenging task. To tackle these challenges, this dissertation develops a novel, unified framework for statically analyzing differentiable programs by coupling abstract interpretation with automatic differentiation. To obtain program analyses with the desired generality, Chapter 2 of this dissertation proposes DeepJ, the first abstract interpretation framework built upon Clarke Generalized Jacobians. By leveraging a generalized notion of derivatives, DeepJ can soundly reason about gradient properties for both differentiable and non-differentiable (but Lipschitz continuous) functions that result from programs with control flow. The need for generality also extends to higher derivatives and richer program abstractions. To enable these extensions, Chapter 3 proposes the first general construction for abstract interpretation of higher-order AD. This construction allows one to automatically build sound abstract interpreters for arbitrary orders of derivatives with general numerical abstract domains for precise analysis of program properties defined over higher derivatives. To obtain the desired precision, Chapter 4 proposes Pasado which is the first automated technique to synthesize precise static analyzers tailored to the structure of AD. By formulating abstract interpretation as a tractable optimization problem, Pasado optimally solves for precise abstractions of groups of multiple nonlinear operations which correspond to the chain rule, product rule, and quotient rule. Since these rules underlie forward and reverse mode AD, Pasado’s generality enables abstract interpretation of both modes. Compared to the prior state of the art, this precision allows Pasado to compute derivative bounds and local Lipschitz constant bounds that are orders of magnitude more precise. In addition, this dissertation shows extensive experimental results in Chapters 2, 3, and 4 highlighting how these static analyses obtain high scalability. These experiments demonstrate how the proposed analyses successfully reason about derivatives of large convolutional neural architectures involving hundreds of thousands of nonlinear operations."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Static analysis of differentiable programs"]}]}],"canonical_facts":{"dc:contributor":["Misailovic, Sasa","Singh, Gagandeep","Marinov, Darko","Hückelheim, Jan"],"dc:creator":["Laurel, Jacob Scott"],"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, Jacob Laurel, accepted the attached license on 2024-12-03 at 11:00.","The student, Jacob Laurel, submitted this Dissertation for approval on 2024-12-03 at 11:39.","This Dissertation was approved for publication on 2024-12-03 at 14:55.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21472 on 2025-03-28 at 14:27:56","Differentiable Programming which includes Automatic Differentiation (AD), serves as the backbone for machine learning and simultaneously pervades many other domains including graphics and scientific computing. Despite AD’s ubiquity, automated formal reasoning about the derivatives AD computes has lagged. The difficulty in developing automated analyses for differentiable programs stems from the fact that these programs use complicated semantics, contain highly nonlinear operations (e.g., the chain rule) and involve thousands of program variables. Thus, developing program analyses for AD that are simultaneously general, precise, and scalable remains a challenging task. To tackle these challenges, this dissertation develops a novel, unified framework for statically analyzing differentiable programs by coupling abstract interpretation with automatic differentiation. To obtain program analyses with the desired generality, Chapter 2 of this dissertation proposes DeepJ, the first abstract interpretation framework built upon Clarke Generalized Jacobians. By leveraging a generalized notion of derivatives, DeepJ can soundly reason about gradient properties for both differentiable and non-differentiable (but Lipschitz continuous) functions that result from programs with control flow. The need for generality also extends to higher derivatives and richer program abstractions. To enable these extensions, Chapter 3 proposes the first general construction for abstract interpretation of higher-order AD. This construction allows one to automatically build sound abstract interpreters for arbitrary orders of derivatives with general numerical abstract domains for precise analysis of program properties defined over higher derivatives. To obtain the desired precision, Chapter 4 proposes Pasado which is the first automated technique to synthesize precise static analyzers tailored to the structure of AD. By formulating abstract interpretation as a tractable optimization problem, Pasado optimally solves for precise abstractions of groups of multiple nonlinear operations which correspond to the chain rule, product rule, and quotient rule. Since these rules underlie forward and reverse mode AD, Pasado’s generality enables abstract interpretation of both modes. Compared to the prior state of the art, this precision allows Pasado to compute derivative bounds and local Lipschitz constant bounds that are orders of magnitude more precise. In addition, this dissertation shows extensive experimental results in Chapters 2, 3, and 4 highlighting how these static analyses obtain high scalability. These experiments demonstrate how the proposed analyses successfully reason about derivatives of large convolutional neural architectures involving hundreds of thousands of nonlinear operations."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/127261"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Jacob Scott Laurel"],"dc:subject":["Static Analysis","Differentiable Programming","Automatic Differentiation","Abstract Interpretation","Programming Languages"],"dc:title":["Static analysis of differentiable programs"],"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"}