{"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":1773478964338,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":49,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819535842","type":"print"},{"value":"9789819535859","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-3585-9_9","type":"book-chapter","created":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:06:43Z","timestamp":1761804403000},"page":"173-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Checking Consistency of\u00a0Event-Driven Traces"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1634-5893","authenticated-orcid":false,"given":"R.","family":"Govind","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1762-8061","authenticated-orcid":false,"given":"Samuel","family":"Grahn","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"issue":"8","key":"9_CR1","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Inf. 54(8), 789\u2013818 (2017)","journal-title":"Acta Inf."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2535838.2535845"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et al.: Tailoring stateless model checking for event-driven multi-threaded programs. In: Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. Lecture Notes in Computer Science, vol. 14216. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_9","DOI":"10.1007\/978-3-031-45332-8_9"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Govind, R., Grahn, S., Thinniyam, R.S.: Checking consistency of event-driven traces. CoRR arxiv:2508.07855 (2025)","DOI":"10.1007\/978-981-95-3585-9_9"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ng, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3(OOPSLA), 150:1\u2013150:29 (2019)","DOI":"10.1145\/3360576"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless Model Checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. PACMPL 2(OOPSLA), 135:1\u2013135:29 (2018)","DOI":"10.1145\/3276505"},{"key":"9_CR8","unstructured":"kernel-mode\u00a0driver architecture., M.I.W.: http:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff557560(v=vs.85).aspx"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Ozkan, B.K., Tasiran, S.: Verifying robustness of event-driven asynchronous programs against concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 170\u2013200. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_7","DOI":"10.1007\/978-3-662-54434-1_7"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: POPL, pp. 626\u2013638. ACM (2017)","DOI":"10.1145\/3009837.3009888"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Krishna, S.N., Mathur, U., Pavlogiannis, A.: How hard is weak-memory testing? Proc. ACM Program. Lang. 8(POPL), 1978\u20132009 (2024)","DOI":"10.1145\/3632908"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in erlang programs. In: ICST, pp. 154\u2013163. IEEE Computer Society (2013)","DOI":"10.1109\/ICST.2013.50"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR14","unstructured":"Cunningham, R., Kohler, E.: Making events less slippery with eel. In: HotOS. USENIX Association (2005)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Dabek, F., Zeldovich, N., Kaashoek, M.F., Mazi\u00e8res, D., Morris, R.: Event-driven programming for robust software. In: ACM SIGOPS European Workshop, pp. 186\u2013189. ACM (2002)","DOI":"10.1145\/1133373.1133410"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Desai, A., Gupta, V., Jackson, E.K., Qadeer, S., Rajamani, S.K., Zufferey, D.: P: safe asynchronous event-driven programming. In: PLDI, pp. 321\u2013332. ACM (2013)","DOI":"10.1145\/2491956.2462184"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Fischer, J., Majumdar, R., Millstein, T.D.: Tasks: language support for event-driven programming. In: PEPM, pp. 134\u2013143. ACM (2007)","DOI":"10.1145\/1244381.1244403"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Ganty, P., Majumdar, R.: Analyzing real-time event-driven programs. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 164\u2013178. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_14","DOI":"10.1007\/978-3-642-04368-0_14"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Gay, D., Levis, P., von Behren, J.R., Welsh, M., Brewer, E.A., Culler, D.E.: The nesc language: a holistic approach to networked embedded systems. In: Cytron, R., Gupta, R. (eds.) PLDI, pp. 1\u201311. ACM (2003)","DOI":"10.1145\/781131.781133"},{"key":"9_CR20","unstructured":"central\u00a0dispatch (GCD)\u00a0reference., A.C.I.G. http:\/\/developer.apple.com\/library\/mac\/#documentation\/performance\/reference\/gcd_libdispatch_ref\/reference\/reference.html"},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Ph.D. thesis, University of Li\u00e8ge (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7. http:\/\/www.springer.com\/gp\/book\/9783540607618","DOI":"10.1007\/3-540-60761-7"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: POPL, pp. 174\u2013186. ACM Press (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the verisoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Hanmer, R.S., Jagadeesan, L.J.: Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using verisoft. In: ISSTA, pp. 124\u2013133. ACM (1998)","DOI":"10.1145\/271771.271800"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Hill, J.L., Szewczyk, R., Woo, A., Hollar, S., Culler, D.E., Pister, K.S.J.: System architecture directions for networked sensors. In: ASPLOS, pp. 93\u2013104. ACM Press (2000)","DOI":"10.1145\/378993.379006"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Jensen, C.S., M\u00f8ller, A., Raychev, V., Dimitrov, D., Vechev, M.T.: Stateless model checking of event-driven applications. In: OOPSLA, pp. 57\u201373. ACM (2015)","DOI":"10.1145\/2814270.2814282"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17:1\u201317:32 (2018)","DOI":"10.1145\/3158105"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022)","DOI":"10.1145\/3498711"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the linux kernel\u2019s hierarchical read-copy-update (tree RCU). In: SPIN, pp. 172\u2013181. ACM (2017)","DOI":"10.1145\/3092282.3092287"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Vafeiadis, V.: GenMC: a model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 427\u2013440. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"9_CR32","unstructured":"LIBASYNC. http:\/\/pdos.csail.mit.edu\/6.824-2004\/async\/"},{"key":"9_CR33","unstructured":"LIBEVENT. http:\/\/monkey.org\/~provos\/libevent\/"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Lukkarinen, A., Malmi, L., Haaranen, L.: Event-driven programming in programming education: a mapping review. ACM Trans. Comput. Educ. 21(1), 1:1\u20131:31 (2021)","DOI":"10.1145\/3423956"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Maiya, P., Gupta, R., Kanade, A., Majumdar, R.: Partial order reduction for event-driven multi-threaded programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 680\u2013697. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_44","DOI":"10.1007\/978-3-662-49674-9_44"},{"key":"9_CR36","unstructured":"Maiya, P., Kanade, A., Majumdar, R.: Droidracer tested apps repository (2014). https:\/\/bitbucket.org\/iiscseal\/droidracer-related-files\/src\/master\/pldi-2014-tested-apps\/"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Maiya, P., Kanade, A., Majumdar, R.: Race detection for android applications. In: PLDI, pp. 316\u2013325. ACM (2014)","DOI":"10.1145\/2594291.2594311"},{"key":"9_CR38","unstructured":"Mazi\u00e8res, D.: A toolkit for user-level file systems. In: Park, Y. (ed.) Proceedings of the General Track: 2001 USENIX Annual Technical Conference, pp. 261\u2013274. USENIX (2001). http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix01\/mazieres.html"},{"key":"9_CR39","unstructured":"Mednieks, Z., Dornin, L., Meike, G.B., Nakamura, M.: Programming Android. O\u2019Reilly Media, Inc., Boston (2012)"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR41","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267\u2013280. USENIX Association (2008)"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking C\/C++11 code. ACM Trans. Program. Lang. Syst. 38(3), 10:1\u201310:51 (2016)","DOI":"10.1145\/2806886"},{"key":"9_CR43","doi-asserted-by":"publisher","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_34","DOI":"10.1007\/3-540-56922-7_34"},{"key":"9_CR44","unstructured":"Project, T.M.: http:\/\/mace.ucsd.edu"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Raychev, V., Vechev, M.T., Sridharan, M.: Effective race detection for event-driven programs. In: OOPSLA, pp. 151\u2013166. ACM (2013)","DOI":"10.1145\/2509136.2509538"},{"issue":"1","key":"9_CR46","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","volume":"8","author":"CA Tovey","year":"1984","unstructured":"Tovey, C.A.: A simplified np-complete satisfiability problem. Disc. Appl. Math. 8(1), 85\u201389 (1984)","journal-title":"Disc. Appl. Math."},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Tun\u00e7, H.C., Abdulla, P.A., Chakraborty, S., Krishna, S., Mathur, U., Pavlogiannis, A.: Optimal reads-from consistency checking for c11-style memory models. Proc. ACM Program. Lang. 7(PLDI), 761\u2013785 (2023)","DOI":"10.1145\/3591251"},{"key":"9_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: PLDI, pp. 250\u2013259. ACM (2015)","DOI":"10.1145\/2737924.2737956"}],"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-981-95-3585-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T18:14:08Z","timestamp":1773425648000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-3585-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"ISBN":["9789819535842","9789819535859"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-3585-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"31 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/track\/aplas-2025\/aplas-2025-aplas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}