{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:05:50Z","timestamp":1725768350435},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_21","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"376-394","source":"Crossref","is-referenced-by-count":8,"title":["Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Kevin","family":"Hoang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Bond, M.D., Coons, K.E., McKinley, K.S.: PACER: proportional detection of data races. In: Programming Language Design and Implementation, pp. 255\u2013268 (2010)","DOI":"10.1145\/1809028.1806626"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Chen, F., Serbanuta, T., Rosu, G.: jPredictor: a predictive runtime analysis tool for java. In: International Conference on Software Engineering, pp. 221\u2013230 (2008)","DOI":"10.1145\/1368088.1368119"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 52\u201365. Springer, Heidelberg (2008)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-02658-4_21","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P., Sorrentino, F.: Meta-analysis for atomicity violations under nested locking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 248\u2013262. Springer, Heidelberg (2009)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P., Razavi, N., Sorrentino, F.: Predicting null-pointer dereferences in concurrent programs. In: Foundations of Software Engineering, p. 47 (2012)","DOI":"10.1145\/2393596.2393651"},{"issue":"11","key":"21_CR6","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/1839676.1839699","volume":"53","author":"C. Flanagan","year":"2010","unstructured":"Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. Commun. ACM\u00a053(11), 93\u2013101 (2010)","journal-title":"Commun. ACM"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Programming Language Design and Implementation, pp. 293\u2013303 (2008)","DOI":"10.1145\/1379022.1375618"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise cfl-reachability for threads communicating via locks. In: International Symposium on Logic in Computer Science, pp. 27\u201336 (2009)","DOI":"10.1109\/LICS.2009.45"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-14295-6_39","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2010","unstructured":"Kahlon, V., Wang, C.: Universal Causality Graphs: A precise happens-before model for detecting bugs in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 434\u2013449. Springer, Heidelberg (2010)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-31424-7_20","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2012","unstructured":"Kahlon, V., Wang, C.: Lock removal for concurrent trace programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 227\u2013242. Springer, Heidelberg (2012)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-14295-6_13","volume-title":"Computer Aided Verification","author":"S. Kundu","year":"2010","unstructured":"Kundu, S., Ganai, M.K., Wang, C.: Contessa: Concurrency testing augmented with symbolic analysis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 127\u2013131. Springer, Heidelberg (2010)"},{"issue":"7","key":"21_CR13","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Li, D., Srisa-an, W., Dwyer, M.B.: SOS: saving time in dynamic race detection with stationary analysis. In: ACM Conference on Object Oriented Programming, Systems, Languages, and Applications, pp. 35\u201350 (2011)","DOI":"10.1145\/2048066.2048072"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural Support for Programming Languages and Operating Systems, pp. 37\u201348 (2006)","DOI":"10.1145\/1168918.1168864"},{"issue":"4","key":"21_CR16","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C.H. Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM\u00a026(4), 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-20398-5_23","volume-title":"NASA Formal Methods","author":"M. Said","year":"2011","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 313\u2013327. Springer, Heidelberg (2011)"},{"issue":"4","key":"21_CR18","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Sen, K., Rosu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: Foundations of Software Engineering, pp. 337\u2013346 (2003)","DOI":"10.1145\/949952.940116"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S.: Using concurrency to check concurrency: Checking serializability in software transactional memory. In: Parallel and Distributed Processing Symposium (2010)","DOI":"10.1109\/IPDPS.2010.5470389"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predictive analysis for detecting serializability violations through trace segmentation. In: Formal Methods and Models for Codesign, pp. 99\u2013108 (2011)","DOI":"10.1109\/MEMCOD.2011.5970516"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: ACM Symposium on Principles of Programming Languages, pp. 423\u2013434 (2011)","DOI":"10.1145\/1925844.1926433"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., Flanagan, C.: Sound predictive race detection in polynomial time. In: ACM Symposium on Principles of Programming Languages, pp. 387\u2013400 (2012)","DOI":"10.1145\/2103621.2103702"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Sorrentino, F., Farzan, A., Madhusudan, P.: PENELOPE: weaving threads to expose atomicity violations. In: Foundations of Software Engineering, pp. 37\u201346 (2010)","DOI":"10.1145\/1882291.1882300"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"von Praun, C., Gross, T.R.: Object race detection. In: ACM Conference on Object Oriented Programming, Systems, Languages, and Applications, pp. 70\u201382 (2001)","DOI":"10.1145\/504311.504288"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: Foundations of Software Engineering, pp. 23\u201332 (2009)","DOI":"10.1145\/1595696.1595702"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-29860-8_2","volume-title":"Runtime Verification","author":"C. Wang","year":"2012","unstructured":"Wang, C., Ganai, M.: Predicting concurrency failures in the generalized execution traces of x86 executables. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol.\u00a07186, pp. 4\u201318. Springer, Heidelberg (2012)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 328\u2013342. Springer, Heidelberg (2010)"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Wang, C., Said, M., Gupta, A.: Coverage guided systematic concurrency testing. In: International Conference on Software Engineering, pp. 221\u2013230 (2011)","DOI":"10.1145\/1985793.1985824"},{"issue":"2","key":"21_CR31","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.\u00a032(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Software Eng."},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Yu, J., Narayanasamy, S.: A case for an interleaving constrained shared-memory multi-processor. In: International Symposium on Computer Architecture, pp. 325\u2013336 (2009)","DOI":"10.1145\/1555815.1555796"}],"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-642-54013-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T23:42:07Z","timestamp":1558827727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}