{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:30Z","timestamp":1774440330789,"version":"3.50.1"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,10,25]],"date-time":"2012-10-25T00:00:00Z","timestamp":1351123200000},"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":[[2013,8]]},"DOI":"10.1007\/s10009-012-0261-y","type":"journal-article","created":{"date-parts":[[2012,10,24]],"date-time":"2012-10-24T17:47:30Z","timestamp":1351100850000},"page":"337-362","source":"Crossref","is-referenced-by-count":2,"title":["Selected dynamic issues in software model checking"],"prefix":"10.1007","volume":"15","author":[{"given":"Viet Yen","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Theo C.","family":"Ruys","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,25]]},"reference":[{"key":"261_CR1","doi-asserted-by":"crossref","unstructured":"Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.: MoonWalker: verification of.NET programs. In : Kowalewski, S., Philippou, A. (eds.). Proceedings of the 15th International Conference on TACAS 2009, York, UK, March, 2009, LNCS, vol. 5505, pp. 170\u2013173. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00768-2_15"},{"key":"261_CR2","doi-asserted-by":"crossref","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D. (eds.) Proceedings of 16th International Conference on Computer Aided Verification (CAV 2004), Boston, MA, USA, LNCS, vol. 3114, pp. 484\u2013487. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"261_CR3","volume-title":"Java Language Specification","author":"K Arnold","year":"2005","unstructured":"Arnold, K., Gosling, J., Holmes, D.: Java Language Specification. Prentice Hall, Englewood Cliffs (2005)"},{"key":"261_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, New York (2008)"},{"key":"261_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th Symposium on Principles of Programming Languages (POPL 2002), pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"issue":"5-6","key":"261_CR6","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: applications to software engineering. Softw. Tools Technol. Transf. (STTT) 9(5-6), 505\u2013525 (2007)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"261_CR7","unstructured":"Cherkassky, B.V., Goldberg, A.V., Silverstein, C.: Buckets, heaps, lists, and monotone priority queues. In: Saks, M. (ed.) Proceedings of the 8th ACM-SIAM Symposium on Discrete Algorithms (SODA\u201997), New Orleans, LA, USA. Society for Industrial and Applied Mathematics, pp. 83\u201392 (1997)"},{"key":"261_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Proceedings of the 10th International Conference on TACAS 2004, Barcelona, ES. LNCS, vol. 2988, pp. 168\u2013176. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"261_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A. Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998), LNCS, vol. 1427, pp. 147\u2013158. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028741"},{"key":"261_CR10","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"261_CR11","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Proceedings of 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, pp. 439\u2013448. ACM, New York (2000)","DOI":"10.1145\/337180.337234"},{"key":"261_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Bandera: a source-level interface for model checking Java programs. In: Proceedings of 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, pp. 762\u2013765. ACM, New Yorl (2000)","DOI":"10.1145\/337180.337625"},{"key":"261_CR13","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1, 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"261_CR14","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Hatcliff, J.: Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Methods Syst Des 25(2\u20133), 199\u2013240 (2004)","DOI":"10.1023\/B:FORM.0000040028.49845.67"},{"key":"261_CR15","unstructured":"ECMA International. Standard ECMA-335: Common Language Infrastructure (CLI), June 2005. http:\/\/www.ecma-international.org\/publications\/standards\/Ecma-335.htm"},{"key":"261_CR16","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: efficiently computing the happens-before relation using locksets. In: Havelund, K., N\u00fa\u00f1ez, M., Rosu, G., Wolff, B. (eds.) Proceedings of First Combined International Workshops on Formal Approaches to Software Testing (FATES 2006) and Runtime Verification (RV 2006), Seattle, WA, USA, LNCS 4262, pp. 193\u2013208. Springer, Berlin (2006)","DOI":"10.1007\/11940197_13"},{"key":"261_CR17","first-page":"110","volume-title":"Proceedings of POPL 2005","author":"C Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of POPL 2005, pp. 110\u2013121. ACM, New York (2005)"},{"key":"261_CR18","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Boston (1995)"},{"key":"261_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems\u2014an Approach to the state-explosion problem. PhD in Computer Science, University of Liege, Nov. 1994. (A revised version has been published as LNCS 1032, Springer (1996))","DOI":"10.1007\/3-540-60761-7"},{"issue":"3","key":"261_CR20","doi-asserted-by":"crossref","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: exploring runtime for.NET\u2014architecture and applications. Electr. Notes Theor. Comput. Sci. (ENTCS) 144(3), 3\u201326 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci. (ENTCS)"},{"issue":"4","key":"261_CR21","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Softw. Tools Technol. Transfer (STTT) 2(4), 366\u2013381 (2000)","journal-title":"Softw. Tools Technol. Transfer (STTT)"},{"key":"261_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Proceedings of the 10th International SPIN Workshop (SPIN 2003), Portland, OR, USA, May 9\u201310, LNCS, vol. 2648, pp. 235\u2013239. Springer, Berlin (2003)","DOI":"10.1007\/3-540-44829-2_17"},{"key":"261_CR23","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of the 3th International SPIN Workshop (SPIN 1997), University of Twente, Enschede, The Netherlands (1997)"},{"key":"261_CR24","volume-title":"The SPIN Model Checker\u2014Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"261_CR25","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Proceedings of the 15th International SPIN Workshop (SPIN 2008), Los Angeles, CA, USA, August, LNCS, vol. 5126, pp. 134\u2013143. Springer, Berlin (2008)"},{"key":"261_CR26","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking. In: Wu, J., Chanson, S.T., Gao, Q (eds.) Proceedings of FORTE\/PSTV 1999, IFIP Conference Proceedings, vol. 156, pp. 481\u2013497. Kluwer, Hingham (1999)","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"261_CR27","doi-asserted-by":"crossref","unstructured":"Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: Proceedings of the 16th International Conference on Automated Software Engineer (ASE 2001), San Diego, USA, November, pp. 254\u2013261. IEEE Computer Society (2001)","DOI":"10.1109\/ASE.2001.989811"},{"issue":"4","key":"261_CR28","doi-asserted-by":"crossref","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. Softw. Tools Technol. Transf. (STTT) 6(4), 302\u2013319 (2004)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"261_CR29","unstructured":"Iosif, R., Sisto, R.: Using garbage collection in model checking. In: Havelund, K., Penix, J., Visser, W. (eds.) Proceedings of the 7th International SPIN Workshop (SPIN 2000), Stanford, CA, USA, LNCS, vol. 1885, pp. 20\u201333. Springer, Berlin (2000)"},{"key":"261_CR30","doi-asserted-by":"crossref","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B., (ed.) Proceedings of the 8th International SPIN Workshop (SPIN 2001), Toronto, Canada, LNCS, vol. 2057, pp. 80\u2013102. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_6"},{"key":"261_CR31","volume-title":"Inside Microsoft.NET IL Assembler","author":"S Lidin","year":"2002","unstructured":"Lidin, S.: Inside Microsoft.NET IL Assembler. Microsoft Press, USA (2002)"},{"issue":"4","key":"261_CR32","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3(4), 184\u2013195 (1960)","journal-title":"Commun. ACM"},{"key":"261_CR33","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Dill, D.L.: An incremental heap canonicalization algorithm. In: Godefroid, P. (ed.) Proceedings of the 12th International SPIN Workshop (SPIN 2005), San Francisco, CA, USA, LNCS, vol. 3639, pp. 28\u201342. Springer, Berlin (2005)","DOI":"10.1007\/11537328_6"},{"key":"261_CR34","unstructured":"Nguyen, V.Y.: Optimising techniques for model checkers. Master\u2019s thesis, University of Twente, Enschede (2007)"},{"key":"261_CR35","doi-asserted-by":"crossref","unstructured":"Nguyen V.Y., Ruys, T.C.: Memoised garbage collection for software model checking. In: Kowalewski S., Philippou A., (eds.) Proceedings of the 15th International Conference on TACAS 2009, York, UK, LNCS, vol. 5505, pp. 201\u2013214. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00768-2_20"},{"key":"261_CR36","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) Proceedings of the 11th International Conference on TACAS 2005, Edinburgh, UK, LNCS, vol. 3440, pp. 93\u2013107. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"issue":"2","key":"261_CR37","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1006\/jagm.1996.0046","volume":"21","author":"G Ramalingam","year":"1996","unstructured":"Ramalingam, G., Reps, T.W.: An incremental algorithm for a generalization of the shortest-path problem. J. Algorithm. 21(2), 267\u2013305 (1996)","journal-title":"J. Algorithm."},{"key":"261_CR38","unstructured":"Ranganath, V.P., Hatcliff, J., Robby: Enabling efficient partial order reductions for model checking object-oriented programs using static calculation of program dependencies. Technical Report SAnToS-TR2007-2, SAnToS Laboratory, CIS Department, Kansas State University (2007)"},{"key":"261_CR39","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: BOGOR: an extensible and highly-modular software model checking framework. In: Proceedings of ESEC\/SIGSOFT FSE, New York, NY, USA, pp. 267\u2013276, ACM Press, New York (2003)","DOI":"10.1145\/949952.940107"},{"key":"261_CR40","doi-asserted-by":"crossref","unstructured":"Ruys, T.C., Aan de Brugh, N.H.M.: MMC: the mono model checker. ENTCS, 190(1):149\u2013160 (2007). (Proceedings of Bytecode, Braga, Portugal (2007))","DOI":"10.1016\/j.entcs.2007.02.066"},{"key":"261_CR41","doi-asserted-by":"crossref","unstructured":"Smith, L.A., Bull, J.M., Obdrz\u00e1lek, J.: A parallel Java grande benchmark suite. In: Proceedings of the 2001 ACM\/IEEE Conference on Supercomputing (SC 2001), pp. 8\u20138. ACM, New York (2001)","DOI":"10.1145\/582034.582042"},{"key":"261_CR42","doi-asserted-by":"crossref","unstructured":"Tillmann, N., Halleux, J.D.: PEX: White box test generation for .NET. In: Beckert, B., Haehnle, R. (eds.) Proceedings of the 2nd International Conference on TAP 2008, Prato, IT, LNCS, vol. 4966, pp. 134\u2013153. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79124-9_10"},{"issue":"2","key":"261_CR43","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. (ASE) 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng. (ASE)"},{"issue":"1","key":"261_CR44","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/s10009-003-0136-3","volume":"6","author":"P Yang","year":"2004","unstructured":"Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the $$\\pi $$ -calculus: model checking mobile processes using tabled resolution. Softw. Tools Technol. Transf. (STTT) 6(1), 38\u201366 (2004)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"261_CR45","doi-asserted-by":"crossref","unstructured":"Yi, X., Wang, J., Yang, X.: Stateful dynamic partial-order reduction. In: Liu, Z., He, J. (eds.) Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM 2006), LNCS, vol. 4260, pp. 149\u2013167. Springer, Berlin (2006)","DOI":"10.1007\/11901433_9"},{"key":"261_CR46","unstructured":"Bandera. http:\/\/bandera.projects.cis.ksu.edu\/"},{"key":"261_CR47","unstructured":"BLAST: Berkeley Lazy Abstraction Software Verification Tool. http:\/\/mtc.epfl.ch\/software-tools\/blast\/"},{"key":"261_CR48","unstructured":"Bogor. http:\/\/bogor.projects.cis.ksu.edu\/"},{"key":"261_CR49","unstructured":"Java PathFinder. http:\/\/javapathfinder.sourceforge.net\/"},{"key":"261_CR50","unstructured":"The Mono Project. http:\/\/www.mono-project.com"},{"key":"261_CR51","unstructured":"MoonWalker. http:\/\/code.google.com\/p\/moonwalker\/"},{"key":"261_CR52","unstructured":".NET Languages. http:\/\/www.dotnetlanguages.net\/"},{"key":"261_CR53","unstructured":"SLAM. http:\/\/research.microsoft.com\/en-us\/projects\/slam\/"}],"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-012-0261-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0261-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0261-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T16:09:27Z","timestamp":1745078967000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0261-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,25]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["261"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0261-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,25]]}}}