Reference
Abstract
An incremental algorithm for model checking progress properties is proposed. It follows from the following insight: any SCC-closed region of a system’s state graph can be represented by a sequence of inductive assertions. Each iteration of the algorithm selects a set of states, called a skeleton, that together satisfy all fairness conditions; it then applies safety model checkers to attempt to connect the states into a reachable fair cycle. If this attempt fails, the resulting learned lemma takes one of two forms: an inductive reachability assertion that shows that at least one state of the skeleton is unreachable, or an inductive wall that defines two SCC-closed regions of the state graph. Subsequent skeletons must be chosen entirely from one side of the wall. Because a lemma often applies more generally than to the one skeleton from which it was derived, property-directed abstraction is achieved. The algorithm is highly parallelizable.
BibTeX
@string{FMCAD = "International Conference on Formal Methods in Computer Aided Design (FMCAD)"}
@inproceedings{fair-fmcad11,
author = {Aaron R. Bradley and Fabio Somenzi and Zyad Hassan and Yan Zhang},
title = {An Incremental Approach to Model Checking Progress Properties},
booktitle = FMCAD,
year = {2011},
}