{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,11]],"date-time":"2024-07-11T22:33:28Z","timestamp":1720737208877},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,6,6]],"date-time":"2012-06-06T00:00:00Z","timestamp":1338940800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s10515-012-0109-4","type":"journal-article","created":{"date-parts":[[2012,6,5]],"date-time":"2012-06-05T11:41:51Z","timestamp":1338896511000},"page":"491-530","source":"Crossref","is-referenced-by-count":7,"title":["JRF-E: using model checking to give advice on eliminating memory model-related bugs"],"prefix":"10.1007","volume":"19","author":[{"given":"Kyung Hee","family":"Kim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tuba","family":"Yavuz-Kahveci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beverly A.","family":"Sanders","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,6]]},"reference":[{"key":"109_CR1","unstructured":"Amino concurrent building blocks (2012). http:\/\/amino-cbbs.sourceforge.net\/"},{"key":"109_CR2","series-title":"LNCS","first-page":"22","volume-title":"TPHOLs 2007","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Sevcik, J.: Formalising Java\u2019s data-race-free guarantee. In: TPHOLs 2007. LNCS, vol.\u00a04732, pp.\u00a022\u201337. Springer, Berlin (2007)"},{"key":"109_CR3","first-page":"97","volume-title":"Principles of Programming Languages","author":"T. Ball","year":"2003","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: Principles of Programming Languages, pp.\u00a097\u2013105 (2003)"},{"key":"109_CR4","first-page":"79","volume-title":"FORTE","author":"S. Basu","year":"2004","unstructured":"Basu, S., Saha, D., Smolka, S.A.: Localizing program errors for simple debugging. In: FORTE, pp.\u00a079\u201396 (2004)"},{"key":"109_CR5","first-page":"480","volume-title":"ICSE","author":"Y. Brun","year":"2004","unstructured":"Brun, Y., Ernst, M.D.: Finding latent code errors via machine learning over program executions. In: ICSE, pp.\u00a0480\u2013490 (2004)"},{"key":"109_CR6","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"CAV \u201908: Proceedings of the 20th International Conference on Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: CAV \u201908: Proceedings of the 20th International Conference on Computer Aided Verification, pp.\u00a0107\u2013120. Springer, Berlin, Heidelberg (2008)"},{"key":"109_CR7","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1512475.1512478","volume-title":"PASTE \u201908: Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","author":"A. De","year":"2008","unstructured":"De, A., Roychoudhury, A., D\u2019Souza, D.: Java memory model aware software validation. In: PASTE \u201908: Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 8\u201314. ACM, New York, NY, USA (2008)"},{"key":"109_CR8","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/1250734.1250762","volume-title":"PLDI \u201907: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"T. Elmas","year":"2007","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware Java runtime. In: PLDI \u201907: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, New York, NY, USA, pp.\u00a0245\u2013255. ACM Press, New York (2007)"},{"key":"109_CR9","volume-title":"Programming Language Design and Implementation","author":"C. Flanagan","year":"2009","unstructured":"Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. In: Programming Language Design and Implementation (2009)"},{"key":"109_CR10","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/1375581.1375618","volume-title":"PLDI","author":"C. Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: PLDI, pp.\u00a0293\u2013303 (2008)"},{"key":"109_CR11","volume-title":"Java Concurrency in Practice","author":"B. Goetz","year":"2006","unstructured":"Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison-Wesley Professional, Reading (2006)"},{"key":"109_CR12","unstructured":"Google concurrent data structures workshop barriers (2012). http:\/\/code.google.com\/p\/concurrent-data-structures-workshop-barriers\/"},{"key":"109_CR13","volume-title":"Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"key":"109_CR14","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"SPIN Workshop on Model Checking of Software","author":"A. Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: SPIN Workshop on Model Checking of Software, pp.\u00a0121\u2013135. Springer, Berlin (2003)"},{"key":"109_CR15","volume-title":"The Art of Multiprocessor Programming","author":"M. Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Mateo (2008)"},{"issue":"3","key":"109_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/s10703-007-0041-6","volume":"31","author":"T.Q. Huynh","year":"2007","unstructured":"Huynh, T.Q., Roychoudhury, A.: Memory model sensitive bytecode verification. Form. Methods Syst. Des. 31(3), 281\u2013305 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"109_CR17","unstructured":"Java Pathfinder (2012). http:\/\/babelfish.arc.nasa.gov\/trac\/jpf"},{"key":"109_CR18","volume-title":"Proceedings of the 24th ACM\/IEEE Conference on Automated Software Engineering","author":"K.H. Kim","year":"2009","unstructured":"Kim, K.H., Yavuz-Kahveci, T., Sanders, B.A.: Precise data race detection in a relaxed memory model using heuristic-based model checking. In: Proceedings of the 24th ACM\/IEEE Conference on Automated Software Engineering (2009a)"},{"key":"109_CR19","doi-asserted-by":"crossref","unstructured":"Kim, K.H., Yavuz-Kahveci, T., Sanders, B.A.: Precise data race detection in a relaxed memory model using model checking. Technical report Rep-2009-480, University of Florida (2009b)","DOI":"10.1109\/ASE.2009.82"},{"issue":"9","key":"109_CR20","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"109_CR21","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1145\/1040305.1040336","volume-title":"POPL \u201905: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"J. Manson","year":"2005","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL \u201905: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, pp.\u00a0378\u2013391. ACM Press, New York (2005)"},{"key":"109_CR22","unstructured":"Musuvathi, M., Qadeer, S., Ball, T.: Chess: a\u00a0systematic testing tool for concurrent software. Technical report MSR-TR-2007-149, Microsoft Research, (2007)"},{"key":"109_CR23","unstructured":"The Java Grande Forum benchmark suite (2012). http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"issue":"2","key":"109_CR24","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.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0109-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-012-0109-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0109-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T07:01:00Z","timestamp":1561791660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-012-0109-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,6]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["109"],"URL":"https:\/\/doi.org\/10.1007\/s10515-012-0109-4","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,6]]}}}