Precise reasoning for programs using containers

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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verication General Terms Languages, Verification, Experimentation

• Type: Journal
• Year: 2011
• Where: POPL
• Authors: Isil Dillig, Thomas Dillig, Alex Aiken
• Keywords: Code Categories, Container Contents, POPL 2011, Precise Analysis, Programming Languages