Formal verification and analysis

With the increase in complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality and reliability. Various techniques for automated and semi-automated analysis and verification have been successfully applied to real-life computer systems. However, these techniques are computationally demanding and memory-intensive in general and their applicability to extremely large and complex systems routinely seen in practice these days is limited. The major hampering factor is the state space explosion problem due to which large industrial models cannot be efficiently handled unless we use more sophisticated and scalable methods and a balance of the usual trade-off between run-time, memory requirements, and precision of a method.

Our goal is to attack the scalability problem by exploiting the capabilities of modern hardware architectures. We are developing methods and techniques that fight memory limits with efficient utilisation of external I/O devices, introduce cluster-based algorithms to employ aggregate power of network-interconnected computers, speed-up the verification on multi-core processors or accelerate verification using GPU devices.

Main research priorities

Research team

The research is performed in the Laboratory for Parallel and Distributed Systems ParaDiSe. The web pages of the laboratory give more detailed and complete picture about our research related activities, including publications, seminars, research projects etc.


prof. Luboš Brim
Telefon: +420-549 49 3647