| Popis: |
In recent years, automated formal verification of software has progressed from a few research labs into large-scale applications, such as cloud infrastructure and smart contracts. Formal verification techniques based on model checking provide the necessary guarantees by exploring systems' behaviour exhaustively and automatically. Moreover, they provide witnesses (explana- tions) for the result of their analysis: a faulty behaviour, if there exists one, or a proof of the absence of such behaviour. However, the general problem that automated software verification is trying to solve is un- decidable. Despite this theoretical barrier, it is quite efficient on many instances that arise in practice. We ascribe this (perhaps surprising) success to a combination of factors: the relentless effort of researchers that come up with new verification procedures to tackle classes of problems where existing techniques struggle; amazing progress in the foundational technologies of satis- fiability solving, especially in Satisfiability Modulo Theories (SMT); and increase of available computational power through parallel and cloud computing. Nevertheless, the growing complex- ity of real-world systems poses new challenges for formal verification, especially for the scalability of the techniques. The task of automated software... |
