Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems¶

Alexander Heußner, Tristan Le Gall, Grégoire Sutre: "Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems", in Corina Păsăreanu (ed.): Proceedings of the 16th Int. Workshop on Model Checking of Software (SPIN 2009), Grenoble, June 2009, LNCS 5578, pp. 107–124, Springer 2009

abstract¶

The technique of counterexample-guided abstraction refinement (Cegar) has been successfully applied in the areas of software and hardware verification. Automatic abstraction refinement is also desirable for the safety verification of complex infinite-state models. This paper in- vestigates Cegar in the context of formal models of network protocols, in our case, the verification of fifo systems. Our main contribution is the introduction of extrapolation-based path invariants for abstraction refinement. We develop a range of algorithms that are based on this novel theoretical notion, and which are parametrized by different extrapolation operators. These are utilized as subroutines in the refinement step of our Cegar semi-algorithm that is based on recognizable partition abstractions. We give sufficient conditions for the termination of Cegar by constraining the extrapolation operator. Our empirical evaluation confirms the benefit of extrapolation-based path invariants.

bibtex¶

@INPROCEEDINGS{heussner-a-2009-107-a,
  author = {Alexander Heu{\ss}ner and Tristan Le Gall and Gr{\'e}goire Sutre},
  title = {Extrapolation-Based Path Invariants for Abstraction Refinement of
    Fifo Systems},
  booktitle = {Proc.\ 16th Int.\ SPIN Workshop on Model Checking Software (SPIN 2009)},
  crossref = {pasareanu-c-2009--a},
  year = {2009},
  pages = {107-124},
  ee = {http://dx.doi.org/10.1007/978-3-642-02652-2_11},
}

@PROCEEDINGS{pasareanu-c-2009--a,
  title = {Model Checking Software, 16th International SPIN Workshop, Grenoble,
    France, June 26-28, 2009. Proceedings},
  year = {2009},
  editor = {Corina S. P\u{a}s\u{a}reanu},
  volume = {5578},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  booktitle = {SPIN},
  ee = {http://dx.doi.org/10.1007/978-3-642-02652-2},
  isbn = {978-3-642-02651-5},
}