Abstract
Symmetry reduction techniques exploit symmetries that occur during the execution of a system in order to minimize its state space for efficient verification of temporal logic properties. This paper presents a framework for concisely defining and evaluating symmetry reductions currently used in software model checking, involving heap objects and processes. An on-the-fly state space exploration algorithm combining both techniques will also be presented. Second, the relation between symmetry and partial-order reductions is investigated, showing how one’s strengths can be used to compensate for the other’s weaknesses. The symmetry reductions presented here were implemented in the dSPIN model-checking tool. We also performed a number of experiments that show significant progress in reducing the cost of finite-state software verification.
Similar content being viewed by others
References
Bayer R, Schkolnick M (1977) Concurrency of operations on B-trees. Acta Informatica 9:1–21
Bosnacki D (2001) Enhancing state space reduction techniques for model checking. PhD Thesis, Technical University of Eindhoven, The Netherlands
Bosnacki D, Dams D, Holenderski L (2002) Symmetric spin. Steffen B, Dwyer M, Pomberger G (eds) Int J Softw Tools Technol Transfer) 4(1):92–106
Clarke EM, Jha S, Enders R, Filkorn T (1996) Exploiting symmetry in temporal logic model checking. Formal Meth Sys Des 9(1/2):77–104
Clarke EM, Grumberg O, Peled D (2001) Model checking. MIT Press, Cambridge, MA
Courcoubetis C, Vardi MY, Wolper P, Yannakakis M (1992) Memory-efficient algorithms for the verification of temporal properties. Formal Meth Sys Des 1(2/3):275–288
Emerson E, Sistla AP (1996) Symmetry and model checking. Formal Meth Sys Des 9(1/2):105–131
Emerson E, Jha S, Peled D (1997) Combining partial order and symmetry reductions. In: Proc. Tools and Algorithms for Construction and Analysis of Systems. Lecture notes in computer science, vol 1217. Springer, Berlin Heidelberg New York, pp 19–34
Gerth R, Kuiper R, Peled D, Penczek W (1995) A partial order approach to branching time logic model checking. In: Proc. 3rd Israel symposium on theory of computing and systems, pp 130–139
Godefroid P (1996) Partial-order methods for the verification of concurrent systems. Lecture notes in computer science, vol 1032. Springer, Berlin Heidelberg New York
Godefroid P (1999) Exploiting symmetry when model-checking software. In: Proc. Formal Methods for Protocol Engineering and Distributed Systems (FORTE/PSTV), pp 257–275
Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32:137–161
Holzmann GJ (1997) The SPIN model checker. IEEE Trans Softw Eng 23:279–295
Holzmann GJ, Peled D (1994) An improvement in formal verification. In: Formal description techniques. Chapman & Hall, London, pp 197–211
Holzmann G, Peled D, Yannakakis M (1996) On nested depth first search. In: Proc. 2nd SPIN workshop
Iosif R (2001) Symmetric model checking for object-based programs. Technical Report KSU CIS TR 2001-5, Kansas State University, Manhattan, KS
Iosif R (2001) Exploiting heap symmetries in explicit-state model checking of software. In: Proc. 16th IEEE conference on automated software engineering, pp 254–261
Iosif R (2002) Symmetry reduction criteria for software model checking. Proc. 9th SPIN workshop. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 22–41
Iosif R (2002) An observational characterization of heap symmetry. Technical Report. http://www-verimag.imag.fr/∼iosif/completness.ps
Iosif R, Sisto R (1999) dSPIN: A dynamic extension of SPIN. In: Proc. 6th SPIN workshop. Lecture notes in computer science, vol 1680. Springer, Berlin Heidelberg New York, pp 261–276
Iosif R, Sisto R (2000) Using garbage collection in model checking. In: Proc. 7th SPIN workshop. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 20–33
Ip C, Dill D (1996) Better verification through symmetry. Formal Meth Sys Des 9(1/2):41–75
Jones ND, Muchnick SS (1981) Flow analysis and optimization of LISP-like structures. In: Program flow analysis: theory and applications. Prentice-Hall, Upper Saddle River, NJ, pp 102–131
Lerda F, Visser W (2001) Addressing dynamic issues of program model checking. In: Proc. 8th SPIN workshop. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York, pp 80–102
Peled D (1993) All from one, one from all: on model checking using representatives. In: Proc. 5th conference on computer aided verification. Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 409–423
Robby, Dwyer MB, Hatcliff J (2003) Bogor: an extensible and highly-modular model checking framework. In: Proc. 4th joint meeting of the European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering
Robby, Dwyer MB, Hatcliff J, Iosif R (2003) Space-reduction strategies for model checking dynamic software. Electron Notes Theor Comput Sci 89(3)
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin Heidelberg New York
Sagiv M, Reps T, Wilhelm R (1998) Solving shape-analysis problems in languages with destructive updating. ACM Trans Programm Lang Sys 20(1):1–50
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Iosif, R. Symmetry reductions for model checking of concurrent dynamic software. Int J Softw Tools Technol Transfer 6, 302–319 (2004). https://doi.org/10.1007/s10009-004-0154-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-004-0154-9