Computer Science

Computer Science Colloquium

Im Rahmen des Informatik-Kolloquiums, das von den Instituten des Fachbereichs Informatik, der Österreichischen Gesellschaft für Informatik (ÖGI), der Arbeitsgemeinschaft für Datenverarbeitung (ADV) sowie der Österreichischen Computergesellschaft (OCG) abgehalten wird, spricht

Daniel Kroening

Oxford University

über das Thema:

Model Checking C++ Programs that use the STL

Zeit: 2009-11-26 09:00:00.0, 60 Minuten
Ort: Johannes Kepler Universität Linz, Hörsaal 9


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.


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.
Liste aller Vorträge
Last modified on Thursday, 01-Jan-1970 01:00:00 CET