Verifying C++ programs that use the STL

  • Autor:

    Prof. Dr. Daniel Kröning

  • Datum: 16.03.2009

Informatik-Sonderkolloquium

Vortragender

Prof. Dr. Daniel Kröning
Oxford University

Zeit

Montag, 16. März 2009, 17:30 Uhr

Ort

Seminarraum 131, Informatik-Hauptgebäude (Geb. 50.34)
Am Fasanengarten 5, 76131 Karlsruhe
Campusplan | Google-Maps

Beschreibung 

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.