VSL Publications

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.
  1. onthefly-extended.pdf (extended version)
Related Links
  1. Experimental Archive page
  Under Construction

VSL | Publications