@inproceedings{44f8dad95c5c47f4a5ae08ef1adbdd58,
title = "Verifying C++ with STL containers via predicate abstraction",
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.",
keywords = "C++, STL, iterator, model checking, predicate abstraction, verification",
author = "Nicolas Blanc and Alex Groce and Daniel Kroening",
year = "2007",
doi = "10.1145/1321631.1321724",
language = "English (US)",
isbn = "9781595938824",
series = "ASE'07 - 2007 ACM/IEEE International Conference on Automated Software Engineering",
pages = "521--524",
booktitle = "ASE'07 - 2007 ACM/IEEE International Conference on Automated Software Engineering",
note = "22nd IEEE/ACM International Conference on Automated Software Engineering, ASE'07 ; Conference date: 05-11-2007 Through 09-11-2007",
}