Publications

Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties

Authors
José Vander Meulen, Charles Pecheur
Tags
, , , ,
Title
Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties
Authors
José Vander Meulen, Charles Pecheur
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
Type
In Proceedings
Book title
NASA FORMAL METHODS 2011
Series
LNCS
Volume
6617
Publisher
Springer
Editor
Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, Rajeev Joshi
Year
2011

Abstract

BDD-based symbolic techniques and partial order reduction (POR) are two fruitful approaches to deal with the combinatorial explosion of model checking. Unfortunately, past experience has shown that BDD-based techniques do not work well for loosely-synchronized models. Whereas, by applying POR methods, explicit-state model checkers are able to deal with large concurrent models. This paper presents an algorithm which combines symbolic model checking and POR to verify linear temporal logic properties (LTL without the next time operator) which performs better on models featuring asynchronous processes. Our algorithm adapts and combines three methods: Lerda et al.'s ImProviso algorithm which incorporates POR in symbolic model checking, Iwashita et al.'s forward symbolic CTL model checking, and Clarke et al.'s symbolic LTL model checking algorithm. We present our algorithm, outline the proof of its correctness, and present a prototypal implementation and an evaluation on two examples.

Tags Tags: , , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2011-1,
    TITLE = {Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties},
    AUTHOR = {José {Vander Meulen} and Charles Pecheur },
    YEAR = {2011},
    VOLUME = {6617},
    PUBLISHER = {Springer},
    EDITOR = {Mihaela Bobaru and Klaus Havelund and Gerard Holzmann and Rajeev Joshi },
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties},
  }