{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:52Z","timestamp":1725533932152},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026515"},{"type":"electronic","value":"9783642026522"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02652-2_22","type":"book-chapter","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T11:43:06Z","timestamp":1245930186000},"page":"279-295","source":"Crossref","is-referenced-by-count":18,"title":["Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis"],"prefix":"10.1007","author":[{"given":"Yu","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaofang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using Verisoft. In: POPL, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"22_CR2","first-page":"446","volume-title":"PLDI","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 446\u2013455. ACM, New York (2007)"},{"key":"22_CR3","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah (2008)"},{"key":"22_CR4","first-page":"110","volume-title":"POPL","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic Partial-order Reduction for Model Checking Software. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 110\u2013121. ACM, New York (2005)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-85114-1_20","volume-title":"Model Checking Software","author":"Y. Yang","year":"2008","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Efficient stateful dynamic partial order reduction. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 288\u2013305. Springer, Heidelberg (2008)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-88387-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Y., Gupta, A., Gopalakrishnan, G.: Dynamic model checking with property driven pruning to detect race conditions. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 126\u2013140. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des.\u00a09(1-2), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"issue":"1-2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des.\u00a09(1-2), 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Des."},{"issue":"1\/2","key":"22_CR9","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design\u00a09(1\/2), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"key":"22_CR10","series-title":"IFIP Conference Proceedings","first-page":"257","volume-title":"FORTE","author":"P. Godefroid","year":"1999","unstructured":"Godefroid, P.: Exploiting symmetry when model-checking software. In: FORTE. IFIP Conference Proceedings, vol.\u00a0156, pp. 257\u2013275. Kluwer, Dordrecht (1999)"},{"issue":"4","key":"22_CR11","doi-asserted-by":"publisher","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. STTT\u00a02(4), 366\u2013381 (2000)","journal-title":"STTT"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-85114-1_22","volume-title":"Model Checking Software","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Joshi, R.: Verifying multi-threaded c programs with SPIN. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 325\u2013342. Springer, Heidelberg (2008)"},{"key":"22_CR13","unstructured":"http:\/\/www.cs.utah.edu\/~yuyang\/inspect\/"},{"key":"22_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"22_CR16","unstructured":"http:\/\/freshmeat.net\/projects\/aget\/"},{"key":"22_CR17","unstructured":"http:\/\/freshmeat.net\/projects\/pfscan"},{"key":"22_CR18","first-page":"731","volume-title":"DAC","author":"F.A. Aloul","year":"2002","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: DAC, pp. 731\u2013736. ACM, New York (2002)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: Building a better boolean matcher and symmetry detector. In: DATE, pp. 1079\u20131084 (2006)","DOI":"10.1109\/DATE.2006.243959"},{"key":"22_CR20","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1145\/996566.996712","volume-title":"DAC","author":"P.T. Darga","year":"2004","unstructured":"Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: DAC, pp. 530\u2013534. ACM, New York (2004)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: SIMA Workshop on Algorithm Engineering and Experiments (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"22_CR22","first-page":"149","volume-title":"DAC","author":"P.T. Darga","year":"2008","unstructured":"Darga, P.T., Sakallah, K.A., Markov, I.L.: Faster symmetry discovery using sparsity of symmetries. In: DAC, pp. 149\u2013154. ACM, New York (2008)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-540-73368-3_43","volume-title":"Computer Aided Verification","author":"T. Wahl","year":"2007","unstructured":"Wahl, T.: Adaptive symmetry reduction. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 393\u2013405. Springer, Heidelberg (2007)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"key":"22_CR25","first-page":"254","volume-title":"16th IEEE International Conference on Automated Software Engineering (ASE 2001)","author":"R. Iosif","year":"2001","unstructured":"Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: 16th IEEE International Conference on Automated Software Engineering (ASE 2001), Coronado Island, San Diego, CA, USA, November 26-29, 2001, pp. 254\u2013261. IEEE Computer Society, Los Alamitos (2001)"},{"issue":"4","key":"22_CR26","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"},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/1146238.1146243","volume-title":"Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006","author":"W. Visser","year":"2006","unstructured":"Visser, W., Pasareanu, C.S., Pel\u00e1nek, R.: Test input generation for java containers using state matching. In: Pollock, L.L., Pezz\u00e8, M. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, pp. 37\u201348. ACM, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02652-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T20:01:04Z","timestamp":1685044864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02652-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026515","9783642026522"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02652-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}