{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T17:04:28Z","timestamp":1732035868461},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_14","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"291-310","source":"Crossref","is-referenced-by-count":2,"title":["Hybrid Analysis for Partial Order Reduction of Programs with Arrays"],"prefix":"10.1007","author":[{"given":"Pavel","family":"Par\u00edzek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-642-12002-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Ball","year":"2010","unstructured":"Ball, T., Burckhardt, S., Coons, K.E., Musuvathi, M., Qadeer, S.: Preemption sealing for efficient concurrency testing. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 420\u2013434. Springer, Heidelberg (2010)"},{"key":"14_CR2","unstructured":"Concurrency Tool Comparison repository. \n                      https:\/\/facwiki.cs.byu.edu\/vv-lab\/index.php\/Concurrency_Tool_Comparison"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"M Dwyer","year":"2004","unstructured":"Dwyer, M., Hatcliff, J., Ranganath, V., Robby, : Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Meth. Syst. Des. 25, 199\u2013240 (2004)","journal-title":"Formal Meth. Syst. Des."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL 2005. ACM (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95\u2013112. Springer, Heidelberg (2007)"},{"key":"14_CR7","unstructured":"The Java Grande Forum Benchmark Suite. \n                      https:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"key":"14_CR8","unstructured":"Java Pathfinder: a system for verification of Java programs. \n                      http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Li, D., Srisa-an, W., Dwyer, M.B.: SOS: saving time in dynamic race detection with stationary analysis. In: Proceedings of OOPSLA 2011. ACM (2011)","DOI":"10.1145\/2048066.2048072"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL 2005. ACM (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Marron, M., Mendez-Lojo, M., Hermenegildo, M., Stefanovic, D., Kapur, D.: Sharing analysis of arrays, collections, and recursive structures. In: Proceedings of PASTE 2008. ACM (2008)","DOI":"10.1145\/1512475.1512485"},{"issue":"1","key":"14_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560581","volume":"39","author":"E Noonan","year":"2014","unstructured":"Noonan, E., Mercer, E., Rungta, N.: Vector-clock based partial order reduction for JPF. ACM SIGSOFT Softw. Eng. Notes 39(1), 1\u20135 (2014)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"14_CR13","unstructured":"pjbench: Parallel Java Benchmarks. \n                      https:\/\/bitbucket.org\/pag-lab\/pjbench"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Parizek, P., Jancik, P.: Approximating happens-before order: interplay between static analysis and state space traversal. In: Proceedings of SPIN 2014. ACM (2014)","DOI":"10.1145\/2632362.2632365"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Parizek, P., Lhotak, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE 2011. IEEE CS (2011)","DOI":"10.1109\/ASE.2011.6100154"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1016\/j.scico.2014.10.008","volume":"98","author":"P Parizek","year":"2015","unstructured":"Parizek, P., Lhotak, O.: Model checking of concurrent programs with static analysis of field accesses. Sci. Comput. Program. 98, 735\u2013763 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"14_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Schaefer, M., Sridharan, M., Dolby, J., Tip, F.: Dynamic determinacy analysis. In: Proceedings of PLDI 2013. ACM (2013)","DOI":"10.1145\/2491956.2462168"},{"issue":"7","key":"14_CR19","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Comm. ACM 53(7), 89\u201397 (2010)","journal-title":"Comm. ACM"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Thomson, P., Donaldson, A., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP 2014. ACM (2014)","DOI":"10.1145\/2555243.2555260"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Unkel, C., Lam, M.S.: Automatic inference of stationary fields: a generalization of Java\u2019s final fields. In: Proceedings of POPL 2008. ACM (2008)","DOI":"10.1145\/1328438.1328463"},{"issue":"2","key":"14_CR22","doi-asserted-by":"publisher","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. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"14_CR23","unstructured":"Wala, T.J.: Watson Libraries for Analysis. \n                      http:\/\/wala.sourceforge.net\/"},{"key":"14_CR24","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.C., Kirby, R.M.: Efficient stateful dynamic partial order reduction. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 288\u2013305. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T04:34:36Z","timestamp":1559363676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}