DiVinE Multi-Core -- A Parallel LTL Model-Checker

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. 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 2008
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords LTL Model Checking; Parallel; Tool
Description We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically for multi-core and multi-cpu environments using shared memory. We show how the parallel algorithms allow the tool to exploit the power of contemporary hardware, which is based on increasing number of CPU cores in a single system, as opposed to increasing speed of a single CPU core.
Related projects:

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