Formal verification of systems – a survey of approaches from classical to recent developments

Engineering systems has always been a challenge, particularly guaranteeing safety, i.e., ensuring that the system behaves precisely as specified. A system in this context can be a classical computer (i.e. desktop or web application) or an embedded system (a system interacting directly with the environment in which it is embedded). It can consist of both hardware and software parts and involve both discrete (as in computing systems) and continuous parts (e.g. physical values as in robotics).

A standard approach for verification is testing. However, it is impossible to explore the entire state space via testing. For safety-critical system parts, approaches to mathematically prove correctness for all possible states – formal verification – has therefore been introduced. In this talk we are 1) providing a survey of the classical approaches during which we also discuss the theoretical thresholds and challenges of formal verification, and 2) discussing recent developments, particularly as system designs and verification methods increasingly involve methods of machine learning, thereby introducing the concept of uncertainty into this domain.