Affiliations: Department Informatik, Carl von Ossietzky
Universität Oldenburg, 26129 Oldenburg, Germany.
[email protected] | Fachrichtung Informatik, Universität des
Saarlandes, 66123 Saarbrücken, Germany. [email protected] | Fachrichtung Informatik, Universität des
Saarlandes, 66123 Saarbräcken, Germany.
[email protected] | Institut für Informatik,
Universität Paderborn, 33098 Paderborn, Germany.
[email protected]
Note: [] Address for correspondence: Fachrichtung Informatik,
Universität des Saarlandes, 66123 Saarbrücken,
Germany
Abstract: Abstraction and slicing are both techniques for reducing the size of
the state space to be inspected during verification. In this paper, we present
a new model checking procedure for infinite-state concurrent systems that
interleaves automatic abstraction refinement, which splits states according to
new predicates obtained by Craig interpolation, with slicing, which removes
irrelevant states and transitions from the abstraction. The effects of
abstraction and slicing complement each other. As the refinement progresses,
the increasing accuracy of the abstract model allows for a more precise slice;
the resulting smaller representation gives room for additional predicates in
the abstraction. The procedure terminates when an error path in the abstraction
can be concretized, which proves that the system is erroneous, or when the
slice becomes empty, which proves that the system is correct.
