{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/127275"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/127275","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Mining specifications in a new world: using a test generator through a learning lens","abstract":"This Dissertation was approved for publication on 2024-12-06 at 10:26.","abstract_html":"This Dissertation was approved for publication on 2024-12-06 at 10:26.","abstract_has_math":false,"creators":["Astorga, Angello"],"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","Xie, Tao","Marinov, Darko","Solar-Lezama, Armando"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-12","date_published":"2024-12","updated_at":"2026-07-22T22:25:03Z","subjects":["One-class Classification","Perception Contracts","Safety","Neural Perception","Precondition","Dynamic Symbolic Execution","Symbolic Analysis","Specification Mining","Data-driven Inference","Synthesis","Software Testing"],"languages":["en","eng"],"rights":["Copyright 2024 Angello Astorga"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/127275","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan","Xie, Tao","Marinov, Darko","Solar-Lezama, Armando"]},{"key":"dc:creator","label":"Author","values":["Astorga, Angello"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-12","2024-12-06"]},{"key":"dc:type","label":"Dc Type","values":["Thesis","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":["One-class Classification","Perception Contracts","Safety","Neural Perception","Precondition","Dynamic Symbolic Execution","Symbolic Analysis","Specification Mining","Data-driven Inference","Synthesis","Software Testing"]}]},{"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 Angello Astorga"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/127275"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This Dissertation was approved for publication on 2024-12-06 at 10:26.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21528 on 2025-03-28 at 14:28:24","In today’s technology-rich world, software systems are deeply intertwined in our daily lives and are increasingly dependent on other software and platforms. When software lacks robustness, failures in a component can cause cascading failures in other code depending on it. To further complicate matters, we are in an era where software can now consist of programmed components interacting with machine-learned models. Annotating programs with specifications such as preconditions and postconditions improves the reliability and robustness of software. A precondition expresses a condition the input must satisfy for the annotated code to behave safely. In 2017, a precondition guarding against unsafe inputs could have been beneficial in avoiding a severe outage. During the debugging of performance issues in the S3 storage services, Amazon engineers invoked a program with incorrect inputs that caused their system to disrupt the availability of various running websites Manually writing specifications is time-consuming and error-prone, even for those with formal methods training. Furthermore, existing specifications in code are limited to basic checks (e.g., nullness) and lack the detail that automated tools can infer Unfortunately, the two predominant philosophies for automatically generating specifications make extreme choices about the quality that the generated specification must carry. The first camp insists on inferring provably correct specifications at the cost of scaling to complex programs. Approaches that ensure provable correctness typically struggle to scale. Often, this kind of inference has to make trade-offs between scaling and the expressiveness of the specification. The other camp insists on scaling and applicability, at the cost of providing provable guarantees. Hence approaches under this umbrella infer likely specifications from program executions typically drawn from a fixed set of tests. The analysis is done without a notion of correctness for the generated specification. At most, the specifications are empirically validated on other sets of tests. This thesis proposes a novel paradigm for automatically mining specifications to fill the gap created by the preceding approaches. This paradigm seeks to strike a balance between the two predominant philosophies on inferring specifications. This thesis builds automated scalable specification mining algorithms that use an automatic test input generator where the inferred specifications are vetted for correctness by the test generator. In establishing a foundation for this paradigm, this thesis includes accompanying problem definitions, novel formalism, learning algorithms, and techniques. Furthermore, the contribution of this thesis includes implementations of these ideas and evaluations further supporting their potential efficacy in practice. We demonstrate the utility of our contribution in object-oriented programs and in systems consisting of programmed components interacting with machine-learned components, more specifically, in systems where neural networks are used to solve perception tasks within a cyber-physical system.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Angello Astorga, accepted the attached license on 2024-12-06 at 09:24.","The student, Angello Astorga, submitted this Dissertation for approval on 2024-12-06 at 09:38."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Mining specifications in a new world: using a test generator through a learning lens"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan","Xie, Tao","Marinov, Darko","Solar-Lezama, Armando"],"dc:creator":["Astorga, Angello"],"dc:date":["2024-12","2024-12-06"],"dc:description":["This Dissertation was approved for publication on 2024-12-06 at 10:26.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21528 on 2025-03-28 at 14:28:24","In today’s technology-rich world, software systems are deeply intertwined in our daily lives and are increasingly dependent on other software and platforms. When software lacks robustness, failures in a component can cause cascading failures in other code depending on it. To further complicate matters, we are in an era where software can now consist of programmed components interacting with machine-learned models. Annotating programs with specifications such as preconditions and postconditions improves the reliability and robustness of software. A precondition expresses a condition the input must satisfy for the annotated code to behave safely. In 2017, a precondition guarding against unsafe inputs could have been beneficial in avoiding a severe outage. During the debugging of performance issues in the S3 storage services, Amazon engineers invoked a program with incorrect inputs that caused their system to disrupt the availability of various running websites Manually writing specifications is time-consuming and error-prone, even for those with formal methods training. Furthermore, existing specifications in code are limited to basic checks (e.g., nullness) and lack the detail that automated tools can infer Unfortunately, the two predominant philosophies for automatically generating specifications make extreme choices about the quality that the generated specification must carry. The first camp insists on inferring provably correct specifications at the cost of scaling to complex programs. Approaches that ensure provable correctness typically struggle to scale. Often, this kind of inference has to make trade-offs between scaling and the expressiveness of the specification. The other camp insists on scaling and applicability, at the cost of providing provable guarantees. Hence approaches under this umbrella infer likely specifications from program executions typically drawn from a fixed set of tests. The analysis is done without a notion of correctness for the generated specification. At most, the specifications are empirically validated on other sets of tests. This thesis proposes a novel paradigm for automatically mining specifications to fill the gap created by the preceding approaches. This paradigm seeks to strike a balance between the two predominant philosophies on inferring specifications. This thesis builds automated scalable specification mining algorithms that use an automatic test input generator where the inferred specifications are vetted for correctness by the test generator. In establishing a foundation for this paradigm, this thesis includes accompanying problem definitions, novel formalism, learning algorithms, and techniques. Furthermore, the contribution of this thesis includes implementations of these ideas and evaluations further supporting their potential efficacy in practice. We demonstrate the utility of our contribution in object-oriented programs and in systems consisting of programmed components interacting with machine-learned components, more specifically, in systems where neural networks are used to solve perception tasks within a cyber-physical system.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Angello Astorga, accepted the attached license on 2024-12-06 at 09:24.","The student, Angello Astorga, submitted this Dissertation for approval on 2024-12-06 at 09:38."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/127275"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Angello Astorga"],"dc:subject":["One-class Classification","Perception Contracts","Safety","Neural Perception","Precondition","Dynamic Symbolic Execution","Symbolic Analysis","Specification Mining","Data-driven Inference","Synthesis","Software Testing"],"dc:title":["Mining specifications in a new world: using a test generator through a learning lens"],"dc:type":["Thesis","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:25:03Z"}