Withdraw
Loading…
Mining specifications in a new world: using a test generator through a learning lens
Astorga, Angello
Loading…
Permalink
https://hdl.handle.net/2142/127275
Description
- Title
- Mining specifications in a new world: using a test generator through a learning lens
- Author(s)
- Astorga, Angello
- Issue Date
- 2024-12-06
- Director of Research (if dissertation) or Advisor (if thesis)
- Parthasarathy, Madhusudan
- Xie, Tao
- Doctoral Committee Chair(s)
- Parthasarathy, Madhusudan
- Xie, Tao
- Committee Member(s)
- Marinov, Darko
- Solar-Lezama, Armando
- Department of Study
- Siebel School Comp & Data Sci
- Discipline
- Computer Science
- Degree Granting Institution
- University of Illinois at Urbana-Champaign
- Degree Name
- Ph.D.
- Degree Level
- Dissertation
- Keyword(s)
- Specification Mining
- Data-Driven Inference
- Synthesis
- Software Testing
- One-Class Classification
- Perception Contracts
- Safety
- Neural Perception
- Precondition
- dynamic symbolic execution
- symbolic analysis
- Abstract
- 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.
- Graduation Semester
- 2024-12
- Type of Resource
- Thesis
- Handle URL
- https://hdl.handle.net/2142/127275
- Copyright and License Information
- Copyright 2024 Angello Astorga
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…