Lectures on Runtime Verification. Introductory and Advanced Topics

International audiencePreface Runtime verification (RV) is a lightweight, yet rigorous, formal method for the monitoring and analysis of the runtime behaviour of software and hardware systems. RV complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach that analyses a single execution trace of a system. At the price of a limited execution coverage, RV can give very precise information on the runtime behaviour of the monitored system. RV is now widely employed in both academia and industry both before system deployment, for testing, verification, and debugging purposes, and after deployment to ensure reliability, safety, robustness and security. The interest on this field of research has grown since 2001 when the first international workshop on RV was organized. This venue has occurred each year since then, becoming a conference in 2010. In 2014, we have initiated the international Competition on Runtime Verification (CRV) with the goal to foster the comparison and evaluation of software runtime verification tools. In the same year, a European scientific network for the COoperation in Science and Technology (COST) on " Runtime Verification beyond Monitoring (ARVI) " was approved and funded within the European framework programme Horizon 2020. ARVI currently includes the participation of scientists from 26 European countries and Australia. In 2016, together with other partners of ARVI, we have also started to organize the first of a series of Schools on RV. Our aim is to train the researchers from academia and industry introducing them first to the basic concepts and then to the advanced topics of this exciting research area