Sciweavers

Share
ASM
2010
ASM

A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking

8 years 10 months ago
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking
Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
Edd Turner, Michael J. Butler, Michael Leuschel
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where ASM
Authors Edd Turner, Michael J. Butler, Michael Leuschel
Comments (0)
books