On partial state matching

Title:

On partial state matching

Authors:

P. Jančík, J. Kofroň

Publication:

Formal Aspects of Computing 29 (5)

DOI:

Year:

2017

Abstract:

During explicit software model checking, the tools spend a lot of time in state matching. This is implied not only by processing a huge number of states, but also by the fact that state representation is usually not small either. In this article, we present two dead variable analyses; applying them during the code-model-checking process results in size reduction of both state representation and explored state space itself. We implemented the analyses inside Java PathFinder and evaluate their impact in terms of memory and time reduction using several non-trivial benchmarks.

BibTeX:

@article{jancik_partial_2017,
    title = {{On partial state matching}},
    author = {Jančík, Pavel and Kofroň, Jan},
    year = {2017},
    journal = {{Formal Aspects of Computing}},
    number = {5},
    doi = {10.1007/s00165-016-0413-z},
    issn = {1433-299X},
    pages = {777--803},
    volume = {29},
}