Data-driven verification
Abstract/Contents
- Abstract
- Automatic software verification is an important but hard problem. Verifiers primarily rely on static analysis to reason about all possible program behaviors, where a purely static analysis makes inferences based solely on program text. However, since verification is so hard, to be successful it seems necessary to leverage all possible sources that can provide any useful information about the program. Hence, limiting a verifier to just the program text is unnecessarily restrictive. Our thesis is that verification can be aided and significantly improved by learning from data gathered from program executions. In particular, we focus on the problem of invariant inference and its applications in verification. Invariant inference is a core problem that every software verifier must address. The traditional verifiers infer invariants by analyzing program text alone. The main contribution of this thesis is an effective technique to infer loop invariants by combining static analysis and machine learning applied to program executions.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2016 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Sharma, Rahul | |
|---|---|---|
| Associated with | Stanford University, Department of Computer Science. | |
| Primary advisor | Aiken, Alexander | |
| Thesis advisor | Aiken, Alexander | |
| Thesis advisor | Dill, David L | |
| Thesis advisor | Mitchell, John | |
| Advisor | Dill, David L | |
| Advisor | Mitchell, John |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Rahul Sharma. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2016. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2016 by Rahul Sharma
- 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...