We describe a flexible and easily extensible predicate abstraction-based approach to the verification of STL usage, and observe the advantages of verifying programs in terms of high-level data structures rather than low-level pointer manipulations. We formalize the semantics of the STL by means of a Hoare-style axiomatization.
The verification requires an operational model conservatively approximating the semantics given by the C++ standard. Our results show advantages (in terms of errors detected and false positives avoided) over previous attempts to analyze STL usage. |