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
ü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.