Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-11811-1_18 | ASM |
Keywords | Field | DocType |
prob model checker,retrospective b development,model checking technique,state symmetry,b refinement,refinement-based correctness proof,redundant state space exploration,standard model checking,state space explosion,symmetry reduction,previous work,standard model,state space,model checking,b,refinement | Standard Model,Abstraction model checking,Model checking,Correctness proofs,Computer science,Algorithm,Theoretical computer science,Symmetry reduction,Soundness,State space,Homogeneous space | Conference |
Volume | ISSN | ISBN |
5977 | 0302-9743 | 3-642-11810-0 |
Citations | PageRank | References |
7 | 0.48 | 11 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Edd Turner | 1 | 56 | 3.38 |
| Michael Butler | 2 | 1768 | 104.74 |
| Michael Leuschel | 3 | 2156 | 135.89 |