Scalable shared memory LTL model checking

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BRIM Luboš ROČKAI Petr

Year of publication 2010
Type Article in Periodical
Magazine / Source International Journal on Software Tools for Technology Transfer (STTT)
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1007/s10009-010-0136-z
Doi http://dx.doi.org/10.1007/s10009-010-0136-z
Field Informatics
Keywords LTL Model Cecking; Parallel; Shared-Memory
Description Recent development in computer hardware has brought more wide-spread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks - model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experi- ments we conoducted to analyze the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison to sequential tools, which improves the workflow of verification in general.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.