{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T20:29:27Z","timestamp":1672259367893},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2004,8,1]],"date-time":"2004-08-01T00:00:00Z","timestamp":1091318400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,8]]},"DOI":"10.1007\/s10009-004-0154-9","type":"journal-article","created":{"date-parts":[[2004,11,4]],"date-time":"2004-11-04T15:54:04Z","timestamp":1099583644000},"page":"302-319","source":"Crossref","is-referenced-by-count":16,"title":["Symmetry reductions for model checking of concurrent dynamic software"],"prefix":"10.1007","volume":"6","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,11,5]]},"reference":[{"key":"154_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00263762","volume":"9","author":"Bayer","year":"1977","unstructured":"Bayer R, Schkolnick M (1977) Concurrency of operations on B-trees. Acta Informatica 9:1\u201321","journal-title":"Acta Informatica"},{"key":"154_CR2","unstructured":"Bosnacki D (2001) Enhancing state space reduction techniques for model checking. PhD Thesis, Technical University of Eindhoven, The Netherlands"},{"key":"154_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013106","DOI":"10.1007\/s100090200074"},{"key":"154_CR4","doi-asserted-by":"crossref","unstructured":"Clarke EM, Jha S, Enders R, Filkorn T (1996) Exploiting symmetry in temporal logic model checking. Formal Meth Sys Des 9(1\/2):77\u2013104","DOI":"10.1007\/BF00625969"},{"key":"154_CR5","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Peled D (2001) Model checking. MIT Press, Cambridge, MA","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"154_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013288","DOI":"10.1007\/BF00121128"},{"key":"154_CR7","doi-asserted-by":"crossref","unstructured":"Emerson E, Sistla AP (1996) Symmetry and model checking. Formal Meth Sys Des 9(1\/2):105\u2013131","DOI":"10.1007\/BF00625970"},{"key":"154_CR8","doi-asserted-by":"crossref","unstructured":"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\u201334","DOI":"10.1007\/BFb0035378"},{"key":"154_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013139","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"154_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid P (1996) Partial-order methods for the verification of concurrent systems. Lecture notes in computer science, vol 1032. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-60761-7"},{"key":"154_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid P (1999) Exploiting symmetry when model-checking software. In: Proc. Formal Methods for Protocol Engineering and Distributed Systems (FORTE\/PSTV), pp 257\u2013275","DOI":"10.1007\/978-0-387-35578-8_15"},{"key":"154_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"Hennessy","year":"1985","unstructured":"Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32:137\u2013161","journal-title":"J ACM"},{"key":"154_CR13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The SPIN model checker. IEEE Trans Softw Eng 23:279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"154_CR14","unstructured":"Holzmann GJ, Peled D (1994) An improvement in formal verification. In: Formal description techniques. Chapman & Hall, London, pp 197\u2013211"},{"key":"154_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann G, Peled D, Yannakakis M (1996) On nested depth first search. In: Proc. 2nd SPIN workshop","DOI":"10.1090\/dimacs\/032\/03"},{"key":"154_CR16","unstructured":"Iosif R (2001) Symmetric model checking for object-based programs. Technical Report KSU CIS TR 2001-5, Kansas State University, Manhattan, KS"},{"key":"154_CR17","doi-asserted-by":"crossref","unstructured":"Iosif R (2001) Exploiting heap symmetries in explicit-state model checking of software. In: Proc. 16th IEEE conference on automated software engineering, pp 254\u2013261","DOI":"10.1109\/ASE.2001.989811"},{"key":"154_CR18","doi-asserted-by":"crossref","unstructured":"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\u201341","DOI":"10.1007\/3-540-46017-9_5"},{"key":"154_CR19","unstructured":"Iosif R (2002) An observational characterization of heap symmetry. Technical Report. http:\/\/www-verimag.imag.fr\/\u223ciosif\/completness.ps"},{"key":"154_CR20","unstructured":"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\u2013276"},{"key":"154_CR21","doi-asserted-by":"crossref","unstructured":"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\u201333","DOI":"10.1007\/10722468_2"},{"key":"154_CR22","unstructured":"Ip C, Dill D (1996) Better verification through symmetry. Formal Meth Sys Des 9(1\/2):41\u201375"},{"key":"154_CR23","unstructured":"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\u2013131"},{"key":"154_CR24","doi-asserted-by":"crossref","unstructured":"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\u2013102","DOI":"10.1007\/3-540-45139-0_6"},{"key":"154_CR25","doi-asserted-by":"crossref","unstructured":"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\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"154_CR26","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/949952.940107"},{"key":"154_CR27","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer MB, Hatcliff J, Iosif R (2003) Space-reduction strategies for model checking dynamic software. Electron Notes Theor Comput Sci 89(3)","DOI":"10.1016\/S1571-0661(05)80009-X"},{"key":"154_CR28","first-page":"specification","volume":"systems","author":"Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin Heidelberg New York","journal-title":"The temporal logic of reactive and concurrent"},{"key":"154_CR29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"Sagiv","year":"1998","unstructured":"Sagiv M, Reps T, Wilhelm R (1998) Solving shape-analysis problems in languages with destructive updating. ACM Trans Programm Lang Sys 20(1):1\u201350","journal-title":"ACM Trans Programm Lang Sys"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0154-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0154-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0154-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T19:55:20Z","timestamp":1585943720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0154-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["154"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0154-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}