A modular and symbolic approach to static program analysis
Abstract/Contents
- Abstract
- This thesis presents novel static analysis techniques for improving the quality of real-world software. The static analysis techniques we describe are immediately useful for uncovering errors in real code bases, as they are fully automatic, report few false alarms, and scale to large applications. The underlying machinery that allows us to develop these analyses is comprised of a symbolic SAT and SMT-based encoding of program states as well as modular, one function-at-a-time reasoning about the program. More specifically, the contributions of this thesis are four-fold: The first contribution is a static inconsistency detection algorithm that uncovers inconsistent assumptions made by the programmer in a semantic way. Second, we present a novel and sound algorithm that performs an interprocedurally path-sensitive analysis that is capable of giving exact answers to may and must queries about the program with respect to a user-provided, finite abstraction. Third, we describe the first fully modular, summary-based pointer analysis that can systematically perform strong updates to abstract memory locations reachable through function arguments. Finally, this thesis describes an on-line constraint simplification algorithm that significantly improves the scalability of constraint-based program analysis techniques, such as the analyses outlined above.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2011 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Dillig, Thomas Walter |
|---|---|
| Associated with | Stanford University, Computer Science Department |
| Primary advisor | Aiken, Alexander |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Dill, David L |
| Thesis advisor | Sagiv, Mooly |
| Advisor | Dill, David L |
| Advisor | Sagiv, Mooly |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Thomas Dillig. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph. D.)--Stanford University, 2011. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2011 by Thomas Walter Dillig
- 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...