The goal of the project is to contribute to the development of methods for automated verification of infinite-state systems such that their current limitations both in the sense of efficiency as well as generality are reduced as much as possible. (en)
Cílem projektu je přispět k výzkumu metod model checkingu nekonečně stavových systémů tak, aby byly v co největší míře odstraněny jejich současná omezení jak v oblasti efektivity, tak v oblasti obecnosti.
V projektu byla vyvinuta řada technik zvyšujících efektivitu, obecnost a míru automatizace formální verifikace nekonečně stavových systémů, jako jsou programy s ukazateli či poli, pomocí logik a automatů (zejména pak nedeterministických a čítačových). (cs)
The project contributed multiple techniques increasing efficiency, generality, and automation of methods of formal verification of infinite-state systems, such as programs with pointers or arrays, using (nondeterministic and sounter) automata and logics. (en)