Home | Sitemap | Kontakt | english | Impressum | KIT
Informatik mit Profil.
Facebook Google+ Twitter YouTube
KIT on on iTunes U
Immer auf dem Laufenden - mit unserem RSS-Angebot
RSS-Feed

Unsere Nachrichten stehen auch als RSS-Newsfeed zur Verfügung.
RSS-Feed abonnieren

Liste der Kolloquien

2009

2008

Verifying C++ programs that use the STL

Verifying C++ programs that use the STL
Autor:

Prof. Dr. Daniel Kröning

Links:
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.