On combinations of static and dynamic analysis – Panel introduction

Martin Leucker*

*Corresponding author for this work


Model checking [1] deals with the problem of deciding whether all runs of a system under scrutiny satisfy a given specification. As typically infinite runs of the system are of interest, a dynamic analysis of complete runs is not possible. Hence, model checking is necessarily a static analysis technique. Runtime verification [2] on the other hand concentrates on prefixes of runs of the system as it typically considers the actual, necessarily finite run of the system. So while both model checking and runtime verification focus on runs of the system under scrutiny they have a different focus and are applied on a different level of abstraction. In this presentation we elaborate on the similarities and differences of model checking and runtime verification, yet, we mainly introduce question but questions to be studied in the future. We recall the work pointed out in [3] putting runtime verification and (LTL-based) model checking into the same formal framework.

Original languageEnglish
Title of host publicationISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
EditorsTiziana Margaria, Bernhard Steffen
Number of pages2
Volume9952 LNCS
PublisherSpringer, Cham
Publication date05.10.2016
ISBN (Print)978-3-319-47165-5
ISBN (Electronic)978-3-319-47166-2
Publication statusPublished - 05.10.2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Grecotel Corfu Imperial, Kerkira, Greece
Duration: 10.10.201614.10.2016
Conference number: 185089


Dive into the research topics of 'On combinations of static and dynamic analysis – Panel introduction'. Together they form a unique fingerprint.

Cite this