What's wrong with on-the-fly partial order reduction
Stephen F. Siegel. What's wrong with on-the-fly partial
order reduction. In Computer Aided
Verification, Proceedings, 2019.
Partial order reduction and
on-the-fly model checking are well-known approaches for
improving model checking performance. The two optimizations
interact in subtle ways, so care must be taken when using
them in combination. A standard algorithm combining the two
optimizations, published over twenty years ago, has been
widely studied and deployed in popular model checking tools.
Yet the algorithm is incorrect. Counterexamples were
discovered using the Alloy analyzer. A fix for a restricted
class of property automata is proposed.
VSL | Publications