Verifying C++ with STL containers via predicate abstraction

Nicolas Blanc, Alex Groce, Daniel Kroening

Abstract

This paper describes a flexible and easily extensible predicate abstraction-based approach to the verification of STLusage, and observes the advantages of verifying programsin terms of high-level data structures rather than low-level pointer manipulations. We formalize the semantics of theSTL by means of a Hoare-style axiomatization. The verification requires an operational model conservatively approximating the semantics given by the Standard. Our results show advantages (in terms of errors detected and false positives avoided) over previous attempts to analyze STL usage, due to the power of the abstraction engine and model checker

BibTeX

@inproceedings{Blanc-al:ASE07,
  author    = {Nicolas Blanc and
               Alex Groce and
               Daniel Kroening},
  title     = {Verifying C++ with {STL} containers via predicate abstraction},
  booktitle = {ASE},
  pages     = {521--524},
  publisher = {{ACM}},
  year      = {2007},
}

Verifying C++ with STL containers via predicate abstraction

Abstract

Related papers