{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:22:58Z","timestamp":1743117778247,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731955"},{"type":"electronic","value":"9783540731962"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73196-2_8","type":"book-chapter","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T04:50:02Z","timestamp":1183697402000},"page":"112-127","source":"Crossref","is-referenced-by-count":1,"title":["State Isomorphism in Model Programs with Abstract Data Structures"],"prefix":"10.1007","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juhan","family":"Ernits","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Campbell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","first-page":"1","volume-title":"Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic","author":"A. Blass","year":"2000","unstructured":"Blass, A., Gurevich, Y.: Background, reserve, and gandy machines. In: Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, London, UK, pp. 1\u201317. Springer-Verlag, Heidelberg (2000)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10722468_1","volume-title":"SPIN Model Checking and Software Verification","author":"D. Bosnacki","year":"2000","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification. LNCS, vol.\u00a01885, pp. 1\u201319. Springer, Heidelberg (2000)"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566171.566191","volume":"27","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. SIGSOFT Softw. Eng. Notes\u00a027(4), 123\u2013133 (2002)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"8_CR4","unstructured":"Campbell, C., Veanes, M.: State exploration with multiple state groupings. In: Beauquier, D., B\u00f6rger, E., Slissenko, A. (eds.) 12th International Workshop on Abstract State Machines, ASM\u201905, pp. 119\u2013130. Laboratory of Algorithms, Complexity and Logic, Cr\u00e9teil, France (March 2005)"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/1167473.1167504","volume-title":"OOPSLA \u201906","author":"P.T. Darga","year":"2006","unstructured":"Darga, P.T., Boyapati, C.: Efficient software model checking of data structure properties. In: OOPSLA \u201906. Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pp. 363\u2013382. ACM Press, New York, NY, USA (2006)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-48234-2_20","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sisto, R.: dSPIN: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol.\u00a01680, pp. 261\u2013276. Springer, Heidelberg (1999)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The Murphi verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"key":"8_CR8","unstructured":"Fortin, S.: The graph isomorphism problem (1996)"},{"key":"8_CR9","series-title":"Software Engineering Notes","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1145\/566172.566190","volume-title":"ISSTA\u201902","author":"W. Grieskamp","year":"2002","unstructured":"Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: ISSTA\u201902. Software Engineering Notes, vol.\u00a027, pp. 112\u2013122. ACM Press, New York (2002)"},{"issue":"3","key":"8_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2006.01.002","volume":"144","author":"W. Grieskamp","year":"2006","unstructured":"Grieskamp, W., Tillmann, N., Schulte, W.: XRT \u2014 exploring runtime for.Net architecture and applications. Electr. Notes Theor. Comput. Sci.\u00a0144(3), 3\u201326 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"8_CR11","first-page":"9","volume-title":"Evolving Algebras 1993: Lipari Guide (chapter)","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Specification and Validation Methods. In: Evolving Algebras 1993: Lipari Guide (chapter), pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"issue":"4","key":"8_CR12","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/s10009-004-0154-9","volume":"6","author":"R. Iosif","year":"2004","unstructured":"Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT\u00a06(4), 302\u2013319 (2004)","journal-title":"STTT"},{"issue":"1-2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dil, D.L.: Better verification through symmetry. Form. Methods Syst. Des.\u00a09(1-2), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press (Forthcoming 2007)","DOI":"10.1017\/CBO9780511619540"},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/0022-0000(82)90009-5","volume":"25","author":"E.M. Luks","year":"1982","unstructured":"Luks, E.M.: Isomorphism of graphs of bounded valence can be tested in polynomial time. J. Comput. Syst. Sci.\u00a025(1), 42\u201365 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR16","first-page":"45","volume":"30","author":"B.D. McKay","year":"1981","unstructured":"McKay, B.D.: Practical graph isomorphism. Congressus Numerantium\u00a030, 45\u201387 (1981)","journal-title":"Congressus Numerantium"},{"key":"8_CR17","unstructured":"Messmer, B.T.: Efficient graph matching algorithms (1995)"},{"issue":"3","key":"8_CR18","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"38","author":"A. Miller","year":"2006","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv.\u00a038(3), 8 (2006)","journal-title":"ACM Comput. Surv."},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_6","volume-title":"Model Checking Software","author":"M. Musuvathi","year":"2005","unstructured":"Musuvathi, M., Dill, D.L.: An incremental heap canonicalization algorithm. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol.\u00a03639, Springer, Heidelberg (2005)"},{"key":"8_CR20","first-page":"369","volume-title":"ASE \u201906","author":"M. Robby","year":"2006","unstructured":"Robby, M., Dwyer, B., Hatcliff, J.: Domain-specific model checking using the bogor framework. In: ASE \u201906. Proceedings of the 21st IEEE International Conference on Automated Software Engineering (ASE\u201906), pp. 369\u2013370. IEEE Computer Society, Washington, DC, USA (2006)"},{"key":"8_CR21","unstructured":"SpecExplorer (2006), http:\/\/research.microsoft.com\/SpecExplorer"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/321921.321925","volume":"23","author":"J.R. Ullmann","year":"1976","unstructured":"Ullmann, J.R.: An algorithm for subgraph isomorphism. J. ACM\u00a023(1), 31\u201342 (1976)","journal-title":"J. ACM"},{"key":"8_CR23","volume-title":"Practical Model-Based Testing - A tools approach","author":"M. Utting","year":"2006","unstructured":"Utting, M., Legeard, B.: Practical Model-Based Testing - A tools approach. Elsevier, Amsterdam (2006)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N.: Model-based testing of object-oriented reactive systems with Spec Explorer, Tech. Rep. MSR-TR-2005-59, Microsoft Research. Preliminary version of a book chapter in the forthcoming text book Formal Methods and Testing (2005)","DOI":"10.1007\/11526841_38"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Schulte, W.: Composition of model programs. In: The current proceedings (2007)","DOI":"10.1007\/978-3-540-73196-2_9"},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1081706.1081751","volume-title":"ESEC\/FSE-13","author":"M. Veanes","year":"2005","unstructured":"Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC\/FSE-13. Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 273\u2013282. ACM Press, New York, NY, USA (2005)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-540-31980-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Xie","year":"2005","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A framework for generating object-oriented unit tests using symbolic execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 365\u2013381. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73196-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T21:45:12Z","timestamp":1683927912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73196-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540731955","9783540731962"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73196-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}