Verifying C++ with STL containers via predicate abstraction

Nicolas Blanc, Alex Groce, Daniel Kroening

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationASE'07 - 2007 ACM/IEEE International Conference on Automated Software Engineering
Pages521-524
Number of pages4
DOIs
StatePublished - 2007
Externally publishedYes
Event22nd IEEE/ACM International Conference on Automated Software Engineering, ASE'07 - Atlanta, GA, United States
Duration: Nov 5 2007Nov 9 2007

Publication series

NameASE'07 - 2007 ACM/IEEE International Conference on Automated Software Engineering

Conference

Conference22nd IEEE/ACM International Conference on Automated Software Engineering, ASE'07
Country/TerritoryUnited States
CityAtlanta, GA
Period11/5/0711/9/07

Keywords

  • C++
  • iterator
  • model checking
  • predicate abstraction
  • STL
  • verification

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Software

Fingerprint

Dive into the research topics of 'Verifying C++ with STL containers via predicate abstraction'. Together they form a unique fingerprint.

Cite this