Multi-core Model Checking

Description of research

Model checking is one of the most successful techniques for the automated analysis of a system's design models, or even software. It is used to asses a system's dependability, and is very effective to uncover deep bugs in the design or code of a system.

Unfortunately, model checking is also very resource intensive, both in memory and run-time. Our general research goal is to design new model checking algorithms, and to develop new tools, that make better use of available modern hardware.

The current trend is to have workstations equipped with more processors/cores, rather than to increase clock speeds. Hence we investigate parallel algorithms. In order to use the aggregated memory of multiple workstations, we investigate distributed algorithms. Non-standard solutions, like using external memory (disk) or specialized hardware (stream processors) are under investigation too.

Model checking is to be interpreted quite broadly here. It encompasses: - state space generation - model checking algorithms for logics like CTL, LTL, mu-calculus, including their quantitative extensions - state space reduction algorithms - test case generation algorithms

Advisor(s)

Michael Weber

Jaco van de Pol

Duration

4 years

Project

Multi-Core Model Checking

Funding institution

3TU-CEDICT

Strategic Research Orientation

Dependable Systems and Networks (DSN)

Links to relevant web pages:

http://wwwhome.cs.utwente.nl/~laarman/

Pictures

	CTIT Home > Meet the PhDs > Alfons Laarman
Home CTIT symposium 2013 About CTIT News NIRICT Research Meet the PhDs Working at CTIT Internal Information Conferences Open Calls (updated May 3, 2013) Library and Videos Knowledge Transfer Links Sitemap Search	Multi-core Model Checking Description of research Model checking is one of the most successful techniques for the automated analysis of a system's design models, or even software. It is used to asses a system's dependability, and is very effective to uncover deep bugs in the design or code of a system. Unfortunately, model checking is also very resource intensive, both in memory and run-time. Our general research goal is to design new model checking algorithms, and to develop new tools, that make better use of available modern hardware. The current trend is to have workstations equipped with more processors/cores, rather than to increase clock speeds. Hence we investigate parallel algorithms. In order to use the aggregated memory of multiple workstations, we investigate distributed algorithms. Non-standard solutions, like using external memory (disk) or specialized hardware (stream processors) are under investigation too. Model checking is to be interpreted quite broadly here. It encompasses: - state space generation - model checking algorithms for logics like CTL, LTL, mu-calculus, including their quantitative extensions - state space reduction algorithms - test case generation algorithms Advisor(s) Michael Weber Jaco van de Pol Duration 4 years Project Multi-Core Model Checking Funding institution 3TU-CEDICT Strategic Research Orientation Dependable Systems and Networks (DSN) Links to relevant web pages: http://wwwhome.cs.utwente.nl/~laarman/ Pictures