Automated Formal Verification
Lubos Brim

Formal verification is an important technique to validating of the correct behaviour of computer systems. One of the most significant recent developments in the area of formal verification is the discovery of algorithmic methods for verifying temporal-logic properties of finite-state models of systems. These automated methods are known as model-checking. Model-checking tools are now routinely used in industrial applications.

In the talk an overview of concepts, algorithms and tools for model-checking will be presented. Some prospective research directions will be discussed.