| Model checking is one of the most successful formal techniques for the verification of software and hardware systems. Developed in the beginning of the eighties, nowadays it is used by major companies, like Microsoft and Intel, to improve the quality of their products. Multi-core processors of affordable prices that emerged on the market in 2005 promise to bring low-cost parallel computers on our desktops which will denote a turning point in the area of parallel computing and computer science and engineering in general. The aim of this project is to develop new algorithms for model checking (including probabilistic model checking) that can fully exploit the parallelism of the multi-core machines. The emphasis will be put on efficient algorithms for the so called liveness properties expressed in temporal logics. One of the main application areas of model checking are concurrent systems. Since parallel machines will trigger a growing need of software that exploits concurrency and parallelism, one can expect that the emergence of the multi-core technology will significantly increase the importance of model checking in industry. With the increasing complexity of the software the verification can obviously benefit from an efficient fast mulit-core model checking. We plan to develop prototype implementations of the new algorithms in model checkers, like Spin and its extensions, as well as the probabilistic model checker MRMC. The prototype implementations will be validated on case studies including models of biological systems. |
