16th IEEE International Conference on Automated Software Engineering (ASE'01) Exploiting Heap Symmetries in Explicit-State Model Checking of Software San Diego, California November 26-November 29 ISBN: 0-7695-1426-X
Detecting symmetries in the structure of systems is a well known technique falling in the class of bisimulation (strongly) preserving state space reductions. Previous work in applying symmetries to aid model checking focuses mainly on process topologies and user specified data types. We applied the symmetry framework to model checking object-based programs that manipulate dynamically created objects, and developed a linear-time heuristic for finding the canonical representative of a symmetry equivalence class. The strategy was implemented in the object-based model checker dSPIN and some experiments, yielding encouraging results, have been carried out.
Citation:
Radu Iosif, "Exploiting Heap Symmetries in Explicit-State Model Checking of Software," ase, pp.254, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||