Precise and automatic verification of container-manipulating programs
Abstract/Contents
- Abstract
- A key challenge for program verification systems is precise reasoning about the contents of unbounded data structures. A particularly important and widely-used family of data structures is containers, which support operations for inserting, retrieving, removing, and iterating over sets of elements. Typical examples of containers include arrays, lists, vectors, maps, sets, deques, queues, etc. In this thesis, we propose a novel static analysis technique that allows precise reasoning for container-manipulating programs. We describe a symbolic heap abstraction which integrates reasoning about containers directly into a heap analysis, allowing the technique to precisely track heap objects as they flow in and out of containers. The proposed analysis is fully automatic and practical, scaling to real programs of up to 100,000 lines of code. Furthermore, the abstraction we propose can reason about key-value correlations and supports arbitrary nestings of container data structures. More specifically, in this thesis, we first describe a static analysis for a language with only the most basic kind of container, namely arrays. We then refine this basic analysis to obtain a more precise heap abstraction, which is always guaranteed to be relational. We then generalize the framework used for reasoning about arrays to general-purpose containers, which may not expose a notion of position. The symbolic heap abstraction we describe reduces a large part of the difficulty of reasoning about containers to linear inequalities over integers. Thus, the efficiency of our static analysis is contingent upon practical techniques for solving systems of linear integer inequalities. Another contribution of this thesis is a new and practical algorithm called Cuts-from-Proofs for solving linear inequalities over integers.
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, Ayse Isil |
|---|---|
| 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 | Ays̨e Is̨il Dillig. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph. D.)--Stanford University, 2011. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2011 by Ayse Isil 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...