Mining specifications in a new world: using a test generator through a learning lens

Astorga, Angello

Permalink

https://hdl.handle.net/2142/127275 Copy

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