Scalable Multi-core LTL Model-Checking

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 – among others LTL model checking. In the paper we show a design for a parallel sharedmemory LTL model checker, that is based on a distributed-memory algorithm. To achieve good scalability, we have devised and experimentally evaluated several implementation techniques, which we present in the paper.

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Jiri Barnat, Lubos Brim, Petr Rockai
• Keywords: Architectures Offer Opportunities, LTL Model, LTL Model Checker, SPIN 2007, Theoretical Computer Science