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

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Astorga, Angello

Contributors dc:contributor

• Parthasarathy, Madhusudan
• Xie, Tao
• Marinov, Darko
• Solar-Lezama, Armando

• One-class Classification
• Perception Contracts
• Safety
• Neural Perception
• Precondition
• Dynamic Symbolic Execution
• Symbolic Analysis
• Specification Mining
• Data-driven Inference
• Synthesis
• Software Testing

Statement dc:rights

• Copyright 2024 Angello Astorga

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F127275