Our life is increasingly dependent on the correct functioning of software, and the role of software in complex products is expanding fast. The increase in software complexity is paralleled by the amplified risks connected to its failure. For instance, operating systems that used to trust local applications must now defend themselves against malicious applications. Safety-critical software applications with high levels of risk (such as banking and transportation) must be trustworthy, they need reliable guarantees that they behave as intended. However, in most industrial environments, many constraints (time-to-market, cost, lack of skills, etc.) make unrealistic manual verification, validation and certification. We are in need of technologies that can be deployed within industrial constraints and that offer high levels of guarantees for complex systems.

Static analysis examines software applications without actually executing them. It can perform sophisticated analysis, and does not require test cases or the complete code, making it very useful in industry applications.
However, due to its exhaustive nature, static analysis is difficult to scale for complex data structures without sacrificing the precision. Static analysis has been recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. On the one hand, new theories are　continuously proposed to subsume new computing models of modern software, such as distributed computing and resource-aware computing. On the other hand, techniques to design and implement static analysis tools have improved. The last ten decade witnessed the emergence of a wide range of static analysis tools, which are beyond the advanced prototype level.

Runtime verification is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. Runtime verification has emerged as a practical application of formal verification and performs conventional testing in a less ad-hoc way by building monitors from formal specifications. Runtime verification scales well even when complex data structures are used. It is particularly useful, when exhaustive design time verification is impractical or even impossible, due to, for example, the modern system’s inherent complexity or the lack of availability of comprehensive models. However, the quality of runtime analysis depends on test scenarios, which makes it less robust compared to static analysis. Runtime verification　complements design time static analysis with lightweight verification techniques that check violation of intended properties online. Specifically, the field has been addressing technical challenges of generating efficient monitors from high level specification and of formally specifying recovery actions at the specification level.