2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2001)
San Diego, California
Nov. 26, 2001 to Nov. 29, 2001
Radu Iosif , Kansas State University
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.
Radu Iosif, "Exploiting Heap Symmetries in Explicit-State Model Checking of Software", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 254, 2001, doi:10.1109/ASE.2001.989811