Title: Runtime Verification

Abstract:
This presentation will give a comprehensive overview and introduction to
the field of runtime verification. Starting from a definition of runtime
verification, we develop a taxonomy that explains the different aspects
of runtime verification. We explain the core idea of runtime
verification by showing how monitors can be attached to existing
programs, be used to verify certain aspects of the underlying program as
well as be used to guide the program execution. The main part of the
presentation deals with synthesis techniques that, starting from a high
level correctness specifications, derive suitable monitors
automatically. We start with properties expressed in linear temporal
logic (LTL), first with a semantics on finite traces and then extended
to a semantics over infinite traces.