DiVinE Multi-Core - A Parallel LTL Model-Checker

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.

• Type: Conference
• Year: 2008
• Where: ATVA
• Authors: Jiri Barnat, Lubos Brim, Petr Rockai
• Keywords: ATVA 2008, Cpu Core, Hardware, Shared-memory Enumerative Ltl, Single Cpu Core