{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:17Z","timestamp":1784793797057,"version":"3.55.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. Although prior efforts have aimed to address this limitation, we show that state-of-the-art methods remain inaccurate. In this paper, we propose a novel modeling approach that captures mutex semantics using ordering constraints, enabling accurate deadlock verification within partial-order-based concurrent verification frameworks. We formally prove the correctness of our method and implement it in a prototype tool,\n                    <jats:sc>Deagle-DL<\/jats:sc>\n                    . We evaluate\n                    <jats:sc>Deagle-DL<\/jats:sc>\n                    against a state-of-the-art bounded model checker\n                    <jats:sc>ESBMC<\/jats:sc>\n                    that employs the conventional modeling approach, and a state-of-the-art static analysis tool for deadlock detection. Our experiments show that\n                    <jats:sc>Deagle-DL<\/jats:sc>\n                    significantly outperforms both tools in terms of precision, while maintaining substantial efficiency.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_3","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:24Z","timestamp":1784791104000},"page":"42-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deadlock Verification via\u00a0Ordering-Constrained Mutex Modeling"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0437-9141","authenticated-orcid":false,"given":"Pei","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9171-4997","authenticated-orcid":false,"given":"Zhilei","family":"Han","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3787-0144","authenticated-orcid":false,"given":"Zhihang","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4266-875X","authenticated-orcid":false,"given":"Fei","family":"He","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial Orders for Efficient Bounded Model Checking of\u00a0Concurrent\u00a0Software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 258\u2013272. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_25"},{"key":"3_CR3","volume-title":"Concurrent programming: principles and practice","author":"GR Andrews","year":"1991","unstructured":"Andrews, G.R.: Concurrent programming: principles and practice. Benjamin-Cummings Publishing Co., Inc (1991)"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Bensalem, S., Fernandez, J.C., Havelund, K., Mounier, L.: Confirmation of deadlock potentials detected by runtime analysis. In: Proceedings of the 2006 Workshop on Parallel and Distributed S: Testing and Debugging, pp. 41\u201350 (2006). https:\/\/doi.org\/10.1145\/1147403.1147412","DOI":"10.1145\/1147403.1147412"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11678779_15","volume-title":"Hardware and Software, Verification and Testing","author":"S Bensalem","year":"2006","unstructured":"Bensalem, S., Havelund, K.: Dynamic Deadlock Analysis of Multi-threaded Programs. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 208\u2013223. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11678779_15"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 151\u2013186. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Brunet, P., Gorogiannis, N., Kanovich, M.: A compositional deadlock detector for android java. In: 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 955\u2013966. IEEE (2021). https:\/\/doi.org\/10.1109\/ASE51524.2021.9678572","DOI":"10.1109\/ASE51524.2021.9678572"},{"key":"3_CR8","unstructured":"Butenhof, D.R.: Programming with POSIX threads, Addison-Wesley Professional (1993)"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Cai, Y., Meng, R., Palsberg, J.: Low-overhead deadlock prediction. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, pp. 1298\u20131309 (2020). https:\/\/doi.org\/10.1145\/3377811.3380367","DOI":"10.1145\/3377811.3380367"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Cai, Y., Yun, H., Wang, J., Qiao, L., Palsberg, J.: Sound and efficient concurrency bug prediction. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 255\u2013267 (2021). https:\/\/doi.org\/10.1145\/3468264.3468549","DOI":"10.1145\/3468264.3468549"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Cai, Y., Ye, C., Shi, Q., Zhang, C.: Peahen: Fast and precise static deadlock detection via context reduction. In: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 784\u2013796 (2022). https:\/\/doi.org\/10.1145\/3540250.3549110","DOI":"10.1145\/3540250.3549110"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"EG Coffman","year":"1971","unstructured":"Coffman, E.G., Elphick, M., Shoshani, A.: System deadlocks. ACM Comput. Surv. (CSUR) 3(2), 67\u201378 (1971). https:\/\/doi.org\/10.1145\/356586.356588","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 331\u2013340 (2011). https:\/\/doi.org\/10.1145\/1985793.1985839","DOI":"10.1145\/1985793.1985839"},{"key":"3_CR14","unstructured":"Corporation, O.: Locklint overview. https:\/\/docs.oracle.com\/cd\/E19059-01\/wrkshp50\/805-4947\/6j4m8jrng\/index.html"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: The origin of concurrent programming: from semaphores to remote procedure calls, pp. 65\u2013138. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/978-1-4757-3472-0_2","DOI":"10.1007\/978-1-4757-3472-0_2"},{"issue":"5","key":"3_CR16","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/945445.945468","volume":"37","author":"D Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. ACM SIGOPS Oper. Syst. Rev. 37(5), 237\u2013252 (2003). https:\/\/doi.org\/10.1145\/945445.945468","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Eslamimehr, M., Palsberg, J.: Sherlock: scalable deadlock detection for concurrent programs. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 353\u2013365 (2014). https:\/\/doi.org\/10.1145\/2635868.2635918","DOI":"10.1145\/2635868.2635918"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3579835","volume":"45","author":"H Fan","year":"2023","unstructured":"Fan, H., Sun, Z., He, F.: Satisfiability modulo ordering consistency theory for SC, TSO, and PSO memory models. ACM Trans. Program. Lang. Syst. 45(1), 1\u201337 (2023). https:\/\/doi.org\/10.1145\/3579835","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 888\u2013891 (2018). https:\/\/doi.org\/10.1145\/3238147.3240481","DOI":"10.1145\/3238147.3240481"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-25540-4_19","volume-title":"Computer Aided Verification","author":"N Gavrilenko","year":"2019","unstructured":"Gavrilenko, N., Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 355\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19"},{"key":"3_CR21","unstructured":"Harmim, D., Marcin, V., Pavela, O.: Scalable static analysis using facebook Infer. I, VI-B (2019)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K Havelund","year":"2000","unstructured":"Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245\u2013264. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_15"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"He, F., Sun, Z., Fan, H.: Satisfiability modulo ordering consistency theory for multi-threaded program verification. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 1264\u20131279 (2021). https:\/\/doi.org\/10.1145\/3453483.3454108","DOI":"10.1145\/3453483.3454108"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"He, F., Sun, Z., Fan, H.: Deagle: An SMT-based verifier for multi-threaded programs (Competition contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 424\u2013428. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_25","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"3_CR25","unstructured":"Herlihy, M., Shavit, N., Luchangco, V., Spear, M.: The art of multiprocessor programming, Newnes (2020)"},{"issue":"8","key":"3_CR26","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"issue":"3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/356603.356607","volume":"4","author":"RC Holt","year":"1972","unstructured":"Holt, R.C.: Some deadlock properties of computer systems. ACM Comput. Surv. (CSUR) 4(3), 179\u2013196 (1972). https:\/\/doi.org\/10.1145\/356603.356607","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Huang, J.: UFO: predictive concurrency use-after-free detection. In: Proceedings of the 40th International Conference on Software Engineering, pp. 609\u2013619 (2018). https:\/\/doi.org\/10.1145\/3180155.3180225","DOI":"10.1145\/3180155.3180225"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 337\u2013348 (2014). https:\/\/doi.org\/10.1145\/2594291.2594315","DOI":"10.1145\/2594291.2594315"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Inverso, O., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. In: 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 807\u2013812. IEEE (2015). https:\/\/doi.org\/10.1109\/ASE.2015.108","DOI":"10.1109\/ASE.2015.108"},{"issue":"6","key":"3_CR31","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1542476.1542489","volume":"44","author":"P Joshi","year":"2009","unstructured":"Joshi, P., Park, C.S., Sen, K., Naik, M.: A randomized dynamic program analysis technique for detecting real deadlocks. ACM Sigplan Notices 44(6), 110\u2013120 (2009). https:\/\/doi.org\/10.1145\/1542476.1542489","journal-title":"ACM Sigplan Notices"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Kalhauge, C.G., Palsberg, J.: Sound deadlock prediction. Proc. ACM Program. Lang. 2(OOPSLA), 1\u201329 (2018). https:\/\/doi.org\/10.1145\/3276516","DOI":"10.1145\/3276516"},{"issue":"6","key":"3_CR33","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/3062341.3062374","volume":"52","author":"D Kini","year":"2017","unstructured":"Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear time. ACM SIGPLAN Notices 52(6), 157\u2013170 (2017). https:\/\/doi.org\/10.1145\/3062341.3062374","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Kroening, D., Poetzl, D., Schrammel, P., Wachter, B.: Sound static deadlock analysis for C\/Pthreads. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, pp. 379\u2013390 (2016). https:\/\/doi.org\/10.1145\/2970276.2970309","DOI":"10.1145\/2970276.2970309"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C Bounded Model Checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Ponce-de Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC with memory models as modules. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603021","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"3_CR37","unstructured":"Love, R.: Linux kernel development, Pearson Education (2010)"},{"issue":"1","key":"3_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2560012","volume":"10","author":"L Lu","year":"2014","unstructured":"Lu, L., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H., Lu, S.: A study of linux file system evolution. ACM Trans. Storage (TOS) 10(1), 1\u201332 (2014). https:\/\/doi.org\/10.1145\/2560012","journal-title":"ACM Trans. Storage (TOS)"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 329\u2013339 (2008). https:\/\/doi.org\/10.1145\/1346281.1346323","DOI":"10.1145\/1346281.1346323"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Mathur, U., Pavlogiannis, A., Viswanathan, M.: Optimal prediction of synchronization-preserving races. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434317","DOI":"10.1145\/3434317"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Pavlogiannis, A.: Fast, sound, and effectively complete dynamic race prediction. Proc. ACM Program. Lang. 4(POPL), 1\u201329 (2019). https:\/\/doi.org\/10.1145\/3371085","DOI":"10.1145\/3371085"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: ACM-SIGPLAN Symposium on Programming Language Design and Implementation (2004). https:\/\/doi.org\/10.1145\/996841.996845","DOI":"10.1145\/996841.996845"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82\u201397. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_9"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Roemer, J., Gen\u00e7, K., Bond, M.D.: SmartTrack: efficient predictive race detection. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 747\u2013762 (2020). https:\/\/doi.org\/10.1145\/3385412.3385993","DOI":"10.1145\/3385412.3385993"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"Sales, E., Inverso, O., Tuosto, E.: Accurate static data race detection for C. In: International Symposium on Formal Methods, pp. 443\u2013462. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_23","DOI":"10.1007\/978-3-031-71162-6_23"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Samak, M., Ramanathan, M.K.: Multithreaded test synthesis for deadlock detection. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, pp. 473\u2013489 (2014). https:\/\/doi.org\/10.1145\/2660193.2660238","DOI":"10.1145\/2660193.2660238"},{"issue":"8","key":"3_CR47","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/2692916.2555262","volume":"49","author":"M Samak","year":"2014","unstructured":"Samak, M., Ramanathan, M.K.: Trace driven dynamic deadlock detection and reproduction. ACM SIGPLAN Notices 49(8), 29\u201342 (2014). https:\/\/doi.org\/10.1145\/2692916.2555262","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-35632-2_16","volume-title":"Runtime Verification","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2013","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Chen, F., Ro\u015fu, G.: Maximal Causal Models for Sequentially Consistent Systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 136\u2013150. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_16"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Serebryany, K., Iskhodzhanov, T.: ThreadSanitizer: data race detection in practice. In: Proceedings of the workshop on binary instrumentation and applications, pp. 62\u201371 (2009). https:\/\/doi.org\/10.1145\/1791194.1791203","DOI":"10.1145\/1791194.1791203"},{"key":"3_CR50","unstructured":"Silberschatz, A., Galvin, P.B., Gagne, G.: Operating system concepts essentials, Wiley Publishing (2013)"},{"issue":"1","key":"3_CR51","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/2103621.2103702","volume":"47","author":"Y Smaragdakis","year":"2012","unstructured":"Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., Flanagan, C.: Sound predictive race detection in polynomial time. ACM Sigplan Notices 47(1), 387\u2013400 (2012). https:\/\/doi.org\/10.1145\/2103621.2103702","journal-title":"ACM Sigplan Notices"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-23404-5_13","volume-title":"Model Checking Software","author":"F Sorrentino","year":"2015","unstructured":"Sorrentino, F.: PickLock: A Deadlock Prediction Approach under Nested Locking. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 179\u2013199. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_13"},{"key":"3_CR53","unstructured":"Stallings, W.: Operating Systems: Internals and Design Principles, 9\/e. Pearson IT Certification (2018)"},{"issue":"OOPSLA2","key":"3_CR54","doi-asserted-by":"publisher","first-page":"929","DOI":"10.1145\/3563321","volume":"6","author":"Z Sun","year":"2022","unstructured":"Sun, Z., Fan, H., He, F.: Consistency-preserving propagation for SMT solving of concurrent program verification. Proc. ACM Program. Lang. 6(OOPSLA2), 929\u2013956 (2022). https:\/\/doi.org\/10.1145\/3563321","journal-title":"Proc. ACM Program. Lang."},{"key":"3_CR55","unstructured":"Tanenbaum, A.S., Bos, H.: Modern operating systems. Pearson Education Inc., (2015)"},{"key":"3_CR56","unstructured":"Walia, E.: Operating system concepts, KHANNA PUBLISHING HOUSE (2002)"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Wang, P., Han, Z., Sun, Z., He, F.: The artifacts of DEAGLE-DL (2026). https:\/\/doi.org\/10.5281\/zenodo.19696864","DOI":"10.5281\/zenodo.19696864"},{"key":"3_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-89963-3_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Yin","year":"2018","unstructured":"Yin, L., Dong, W., Liu, W., Li, Y., Wang, J.: YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 422\u2013426. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_25"},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Scheduling constraint based abstraction refinement for weak memory models. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 645\u2013655 (2018). https:\/\/doi.org\/10.1145\/3238147.3238223","DOI":"10.1145\/3238147.3238223"},{"issue":"05","key":"3_CR60","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TSE.2018.2864122","volume":"46","author":"L Yin","year":"2020","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: On scheduling constraint abstraction for multi-threaded program verification. IEEE Trans. Softw. Eng. 46(05), 549\u2013565 (2020). https:\/\/doi.org\/10.1109\/TSE.2018.2864122","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Zhou, J., Silvestro, S., Liu, H., Cai, Y., Liu, T.: UNDEAD: Detecting and preventing deadlocks in production software. In: 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 729\u2013740. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115684","DOI":"10.1109\/ASE.2017.8115684"},{"key":"3_CR62","unstructured":"Zou, M., Du, D., Dong, M., Chen, H.: Using dynamically layered definite releases for verifying the RefFS file system. In: 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24), pp. 629\u2013648 (2024). https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/zou"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:27Z","timestamp":1784791107000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}