Current Topics
- DiVinE – The Distributed Verification Environment
- The Distributed Verification Environment (DiVinE) is a research project whose goal is to bring cluster-based enumerative verification to the general public. In order to reach this goal, many challenging theoretical and technical problems are being solved within the project. Recent hot-topics include, but are not limited to: distributed model-checking, efficient state space generation, load-balancing, and inter-cluster computing.
More information about DiVinE - CoIn – Verification of Component-Based Systems
- The aim of the project is to develop a semantic framework for component-based modeling and describing the dynamic behaviour of components and their interactions. Futhermore, we aim at providing algorithms and techniques for formal verification of their temporal properties. The ultimate goal of the project is to come up with a tool for automatic verification of component-interaction properties of component-based systems.
More information about CoIn - Distributed Verification of Finite-State Probabilistic Systems
- The aim of the project is to develop parallel and distributed methods and algorithms for verification of temporal properties of finite-state probabilistic systems. The ultimate goal of the project is to enrich DiVinE with tools enabling automatic distributed verification of large probabilistic systems.
- CUDA Model Checking
- The CUDA project strives to broaden the reach of platform-dependent model checking one step further by employing new generation of massively parallel architectures which are nowadays widely accessible due to modern General-Purpose Graphics Processing Units (GP GPU). This aim involves design of new and adaptation of existing parallel algorithms to allow efficient utilisation of these SIMD architectures with the ultimate goal being the ability to significantly accelerate the whole model checking process.