Partial-order reduction for multi-core LTL model checking

A. Laarman, A.J. Wijs

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

11 Citaten (Scopus)

Samenvatting

Partial-Order Reduction (POR) is a well-known, successful technique for on-the-fly state space reduction in model checking, as evidenced by the prestigious CAV 2014 award for its pioneers. The combination of POR with LTL model checking is long known to cause the so-called ignoring problem, i.e. relevant behavior is continuously ignored and never selected for exploration. This problem has been solved with increasing sophistication over the years, using various ignoring provisos, which include all necessary actions along cycles in the state space. However, parallel model checking algorithms still suffer from a lack of an efficient solution; the best known ones causing severe decrease in reductions. We present a new parallel ignoring proviso for POR, which solves this issue by exploiting parallel DFS-based algorithms. Its similarity to the sequential solutions allows the combination with sophisticated earlier methods solving the ignoring problem. We prove correctness of the new proviso and empirically show that it maintains good reductions, runtime performance and parallel scalability.
Originele taal-2Engels
TitelHardware and Software: Verification and Testing
Subtitel10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings
RedacteurenE. Yahav
Plaats van productieDordrecht
UitgeverijSpringer
Pagina's267-283
ISBN van geprinte versie978-3-319-13338-6
DOI's
StatusGepubliceerd - 2014

Publicatie series

NaamLecture Notes in Computer Science
Volume8855
ISSN van geprinte versie0302-9743

Vingerafdruk

Duik in de onderzoeksthema's van 'Partial-order reduction for multi-core LTL model checking'. Samen vormen ze een unieke vingerafdruk.

Citeer dit