{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:02:44Z","timestamp":1773478964061,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_7","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"170-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burcu Kulahcioglu","family":"Ozkan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"7_CR1","unstructured":"https:\/\/github.com\/irccloud\/android\/commit\/c81f3374"},{"key":"7_CR2","unstructured":"http:\/\/github.com\/irccloud\/android\/tree\/9e2f5cf04e"},{"key":"7_CR3","unstructured":"F-Droid - Free and Open Source App Repository. http:\/\/f-droid.org\/"},{"key":"7_CR4","unstructured":"Java pathfinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/"},{"key":"7_CR5","unstructured":"https:\/\/github.com\/burcuku\/async-robustness-checker"},{"issue":"1\u20132","key":"7_CR6","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R Alur","year":"2000","unstructured":"Alur, R., McMillan, K.L., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1\u20132), 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-40787-1_26","volume-title":"Runtime Verification","author":"S Arzt","year":"2013","unstructured":"Arzt, S., Rasthofer, S., Bodden, E.: Instrumenting android and Java applications as easy as abc. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 364\u2013381. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40787-1_26"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Bielik, P., Raychev, V., Vechev. M.: Scalable race detection for android applications. In: Proceedings of ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, NY, USA, pp. 332\u2013348. ACM (2015)","DOI":"10.1145\/2814270.2814303"},{"key":"7_CR9","unstructured":"Bocchino, Jr. R.L., Adve, V.S., Adve, S.V., Snir, M.: Parallel programming must be deterministic by default. In: Proceedings of 1st USENIX Conference on Hot Topics in Parallelism, HotPar 2009, CA, USA (2009)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-37036-6_17","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290\u2013309. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-37036-6_17"},{"issue":"6","key":"7_CR11","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1743546.1743572","volume":"53","author":"J Burnim","year":"2010","unstructured":"Burnim, J., Sen, K.: Asserting and checking determinism for multithreaded programs. Commun. ACM 53(6), 97\u2013105 (2010)","journal-title":"Commun. ACM"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/1925844.1926432","volume":"46","author":"M Emmi","year":"2011","unstructured":"Emmi, M., Qadeer, S., Rakamari\u0107, Z.: Delay-bounded scheduling. SIGPLAN Not. 46(1), 411\u2013422 (2011). ISSN 0362-1340","journal-title":"SIGPLAN Not."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Emmi, M., Lal, A., Qadeer, S.: Asynchronous programs with prioritized task-buffers. In: Proceedings of International Symposium on Foundations of Software Engineering, FSE 2012, pp. 48:1\u201348:11. ACM (2012)","DOI":"10.1145\/2393596.2393652"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Ozkan, B.K., Tasiran, S.: Exploiting synchronization in the analysis of shared-memory asynchronous programs. In: Proceedings of International SPIN Symposium on Model Checking of Software, pp. 20\u201329. ACM (2014)","DOI":"10.1145\/2632362.2632370"},{"key":"7_CR15","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. 5123, pp. 52\u201365. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-70545-1_8"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-00768-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 155\u2013169. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00768-2_14"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.scico.2007.12.001","volume":"71","author":"C Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89\u2013109 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/1377492.1377495","volume":"30","author":"C Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: static checking and inference for Java. ACM Trans. Program. Lang. Syst. 30(4), 20 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 293\u2013303 (2008)","DOI":"10.1145\/1379022.1375618"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 175\u2013190. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24622-0_16","DOI":"10.1007\/978-3-540-24622-0_16"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Hsiao, C.-H., Yu, J., Narayanasamy, S., Kong, Z., Pereira, C.L., Pokam, G.A., Chen, P.M., Flinn, J.: Race detection for event-driven mobile applications. In: Proceedings of 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 326\u2013336. ACM (2014)","DOI":"10.1145\/2594291.2594330"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Bocchino Jr. R.L., Adve, V.S., Dig, D., Adve, S.V., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H. and Vakilian, M.: A type and effect system for deterministic parallel Java. In: Proceedings of OOPSLA, pp. 97\u2013116 (2009)","DOI":"10.1145\/1639949.1640097"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Lin, Y., Ra, C., Dig, D.: Retrofitting concurrency for android applications through refactoring. In: Proceedings of International Symposium on Foundations of Software Engineering, FSE 2014, NY, USA, pp. 341\u2013352. ACM (2014)","DOI":"10.1145\/2635868.2635903"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Lin, Y., Okur, S., Dig, D.: Study and refactoring of android asynchronous programming. In: Proceedings of ASE (2015)","DOI":"10.1109\/ASE.2015.50"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Maiya, P., Kanade, A., Majumdar, R.: Race detection for android applications. In: Proceedings of 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 316\u2013325. ACM (2014)","DOI":"10.1145\/2594291.2594311"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Ozkan, B.K., Emmi, M., Tasiran, S.: Systematic asynchrony bug exploration for android apps. In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, pp. 455\u2013461 (2015)","DOI":"10.1007\/978-3-319-21690-4_28"},{"issue":"4","key":"7_CR27","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-00590-9_28","volume-title":"Programming Languages and Systems","author":"C Sadowski","year":"2009","unstructured":"Sadowski, C., Freund, S.N., Flanagan, C.: SingleTrack: a dynamic determinism checker for multithreaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 394\u2013409. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00590-9_28"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Safi, G., Shahbazian, A., Halfond, W.G.J., Medvidovic, N.: Detecting event anomalies in event-based systems. In: Proceedings of International Symposium on Foundations of Software Engineering FSE, pp. 25\u201337. ACM (2015)","DOI":"10.1145\/2786805.2786836"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predicting serializability violations: SMT-based search vs. DPOR-based search. In: Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, Revised Selected Papers, pp. 95\u2013114 (2011)","DOI":"10.1007\/978-3-642-34188-5_11"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Steele, Jr. G.L.: Making asynchronous parallelism safe for the world. In: Proceedings of 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1990, NY, USA, pp. 218\u2013231. ACM (1990)","DOI":"10.1145\/96709.96731"},{"issue":"6","key":"7_CR32","doi-asserted-by":"publisher","first-page":"103","DOI":"10.5381\/jot.2004.3.6.a5","volume":"3","author":"C von Praun","year":"2004","unstructured":"von Praun, C., Gross, T.R.: Static detection of atomicity violations in object-oriented programs. J. Object Technol. 3(6), 103\u2013122 (2004)","journal-title":"J. Object Technol."},{"issue":"2","key":"7_CR33","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. Softw. Eng. 32(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Yi, J., Disney, T., Freund, S.N., Flanagan, C.: Cooperative types for controlling thread interference in Java. In: International Symposium on Software Testing and Analysis, ISSTA, pp. 232\u2013242 (2012)","DOI":"10.1145\/2338965.2336781"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54434-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T18:06:13Z","timestamp":1692727573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}