Beyond deductive inference in program analysis

Placeholder Show Content

Abstract/Contents

Abstract
Program analysis tools help developers ensure the safety and robustness of software systems by automatically reasoning about the program. An important barrier to adoption is that these "automatic" tools oftentimes require costly inputs from the human using the analysis. For example, the user must annotate missing code (e.g., dynamically loaded or binary code) and additionally provide a specification encoding desired program behaviors. The focus of this research is to develop techniques that minimize this manual effort using techniques from machine learning. First, in the verification setting (where the goal is to prove a given correctness property), I describe an algorithm that interacts with the user to identify all relevant annotations for missing code, and show that empirically, the required manual effort is substantially reduced. Second, in the bug-finding setting, I describe an algorithm that improves the ability of random testing by automatically inferring the program input language, and show that it generates much higher quality valid test cases compared to a baseline.

Description

Type of resource text
Form electronic; electronic resource; remote
Extent 1 online resource.
Publication date 2017
Issuance monographic
Language English

Creators/Contributors

Associated with Bastani, Osbert
Associated with Stanford University, Computer Science Department.
Primary advisor Aiken, Alexander
Thesis advisor Aiken, Alexander
Thesis advisor Liang, Percy
Thesis advisor Mitchell, John C
Advisor Liang, Percy
Advisor Mitchell, John C

Subjects

Genre Theses

Bibliographic information

Statement of responsibility Osbert Bastani.
Note Submitted to the Department of Computer Science.
Thesis Thesis (Ph.D.)--Stanford University, 2017.
Location electronic resource

Access conditions

Copyright
© 2017 by Osbert Bastani
License
This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).

Also listed in

Loading usage metrics...