Campus Event Calendar
Event Entry
What and Who
Verifying C++ programs that use the STL
Daniel Kroening
Oxford University
SWS Colloquium
Daniel Kroening received the M.E.~and doctoral degrees in computer
science from the University of Saarland in 1999 and 2001, respectively.
He joined the Model Checking group in the Computer Science Department at
Carnegie Mellon University, Pittsburgh PA, USA, in 2001 as a Post-Doc.
He was an assistant professor at the Swiss Technical Institute (ETH) in
Zurich, Switzerland, from 2004 to 2007. He is now a lecturer at the
Computing Laboratory at Oxford University. His research interests
include automated formal verification of hardware and software systems,
decision procedures, embedded systems, and hardware/software co-design.
AG 2, SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 25 July 2008
11:00
60 Minutes
E1 5
007
Saarbrücken
Abstract
We describes 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.
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.
Contact
Claudia Richter
9325 688
--email hidden
passcode not visible
logged in users only
Claudia Richter, 07/24/2008 10:57 -- Created document.