Verifying systems using net unfoldings to represent the state space is a
process containing two steps: generation of the unfolding and reasoning
about the unfolding. In a recent paper we generalized the notion of
unfoldings to unbounded Petri nets and showed how to capture a symbolic
representation of the state space of these nets, thus completing the first
of the two steps discussed above. We now continue with our experimentation
and show how to reason with the unfolding obtained. In particular, we show
how to use a SAT-solver to solve the coverability problem for unbounded
Petri nets. The results of our experiments show that the use of
unfoldings, in spite of the two-step process, has better time and spece
characteristics than an implementation that does not use unfoldings. In
effect, we provide the firs evidence for the conjecture that the two step
process based on unfoldings could be better than a single step
verification process that considers all interleavings.