Isil Dillig
Alex Aiken
Abstract
Containers are general-purpose data structures that provide functionality for inserting, reading, removing, and iterating over elements. Since many applications written in modern programming languages, such as C++ and Java, use containers as standard building blocks, precise analysis of many programs requires a fairly sophisticated understanding of container contents. In this paper, we present a sound, precise, and fully automatic technique for static reasoning about contents of containers. We show that the proposed technique adds useful precision for verifying real C++ applications and that it scales to applications with over 100,000 lines of code.
Supplemental Material
- Dillig, I., Dillig, T., Aiken, A.: Fluid Updates: Beyond Strong vs. Weak Updates. In: ESOP. (2010) Google Scholar
Digital Library
- Gulwani, S., Musuvathi, M.: Cover Algorithms. In: ESOP. (2008) 193--207 Google ScholarDigital Library
- Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: POPL, ACM (1978) 84--96 Google ScholarDigital Library
- Karr, M.: Affine relationships among variables of a program. A.I. (1976) 133--151Google Scholar
- Kovacs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE 2009. (2009) 470--485 Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: SAIL: Static Analysis Intermediate Language. Stanford University Technical ReportGoogle Scholar
- Dillig, I., Dillig, T., Aiken, A.: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. In: CAV. (2009) Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Small Formulas for Large Programs: On-line Constraint Simplification in Scalable Static Analysis. In: SAS. (2010) Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Sound, Complete and Scalable Path-sensitive Analysis. In: PLDI. (2008) 270--280 Google ScholarDigital Library
- http://www.sgi.com/tech/stl/: C++ standard template libraryGoogle Scholar
- http://sourceforge.net/apps/trac/litesql/: LiteSQLGoogle Scholar
- http://www.inkscape.org/: InkscapeGoogle Scholar
- http://www.digikam.org/: DigikamGoogle Scholar
- http://qt.nokia.com/products/: QT FrameworkGoogle Scholar
- Lam, P., Kuncak, V., Rinard, M.: Hob: A tool for verifying data structure consistency. In: Compiler Construction. 237--241 Google ScholarDigital Library
- Lam, P., Kuncak, V., Rinard, M.: Generalized Typestate Checking for Data Structure Consistency. In: VMCAI. (2005) 430--447 Google ScholarDigital Library
- Kuncak, V., Lam, P., Zee, K., Rinard, M.: Modular Pluggable Analyses for Data Structure Consistency. IEEE Transactions on Software Engineering \textbf32(12) (2006) 988--1005 Google ScholarDigital Library
- Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving Specialized Program Analyses for Certifying Component-client Conformance. In: PLDI. (2002) 94 Google ScholarDigital Library
- Blanc, N., Groce, A., Kroening, D.: Verifying C with STL Containers via Predicate Abstraction. In: IEEE/ACM Conference on Automated software engineering, ACM (2007) 521--524 Google ScholarDigital Library
- Gregor, D., Schupp, S.: STLlint: lifting static checking from languages to libraries. Software Practice and Experience \textbf36(3) (2006) 225 Google ScholarDigital Library
- Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: PLDI, ACM NY, USA (1994) 230--241 Google ScholarDigital Library
- Naik, M., Aiken, A.: Conditional Must not Aliasing for Static Race Detection. In: POPL. (2007) 338 Google ScholarDigital Library
- Fink, S., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective Typestate Verification in the Presence of Aliasing. TOSEM \textbf17(2) (2008) 1--34 Google ScholarDigital Library
- Reps, T.W., Sagiv, S., Wilhelm, R.: Static Program Analysis via 3-Valued Logic. In: CAV. (2004) 15--30Google Scholar
- Shacham, O., Vechev, M., Yahav, E.: Chameleon: Adaptive Selection of Collections. In: PLDI, ACM (2009) 408--418 Google ScholarDigital Library
- Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: Precise and efficient static estimation of program computational complexity. In: POPL. (2009) 127--139 Google ScholarDigital Library
- Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, ACM (2008) 235--246 Google ScholarDigital Library
Index Terms
- Precise reasoning for programs using containers
Recommendations
Precise reasoning for programs using containers
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesContainers are general-purpose data structures that provide functionality for inserting, reading, removing, and iterating over elements. Since many applications written in modern programming languages, such as C++ and Java, use containers as standard ...
Precise shape analysis using field sensitivity
We present a static shape analysis technique to infer the shapes of the heap structures created by a program at run time. Our technique is field sensitive in that it uses field information to compute the shapes. The shapes of the heap structures are ...
Connection Analysis: A Practical Interprocedural Heap Analysis for C
Special issue: selected papers from the eighth international workshop on languages and compilers for parallel computingThis paper presents a practical heap analysis technique, connection analysis, that can be used to disambiguate heap accesses in C programs. The technique is designed for analyzing programs that allocate many disjoint objects in the heap such as ...
Comments