Computer Science Colloquium

Daniel Kroening
Oxford University

Model Checking C++ Programs that use the STL

Thu 26.11.2009, 09:00, 60 minutes
Johannes Kepler Universität Linz, Hörsaal 9

Abstract

We present a formalization of the most relevant abstract data types provided by the standard template library (STL). We also provide an operational model, and outline the proof that the operational model is conservative with respect to our formalization. We conclude with experimental evidence that this model enables the automated verification of significant C++ programs.

Bio

Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbruecken, Germany, 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 appointed as an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, in 2004. Since 2007, he is a Reader at the Computing Laboratory at Oxford University and a fellow of Magdalen College, Oxford. His research interests include automated formal verification of hardware and software systems, decision procedures, embedded systems, and hardware/software co-design.

---

The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).

List of all talks