{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T05:02:10Z","timestamp":1779771730443,"version":"3.53.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032008275","type":"print"},{"value":"9783032008282","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"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-3-032-00828-2_18","type":"book-chapter","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T16:23:21Z","timestamp":1760631801000},"page":"326-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Linearizability of Multi-core Task Management and Scheduling System"],"prefix":"10.1007","author":[{"given":"Qiaowen","family":"Jia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Liangjie","family":"Lv","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuting","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jifeng","family":"Hao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hong","family":"Ye","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,17]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS 12, 463\u2013492 (1990)","journal-title":"TOPLAS"},{"key":"18_CR2","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, 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Long, Z., Zhang, Y.: Checking linearizability with fine-grained traces. In: SAC 2016, pp. 1394\u20131400. ACM (2016)","DOI":"10.1145\/2851613.2851774"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"e3928","DOI":"10.1002\/cpe.3928","volume":"29","author":"G Lowe","year":"2017","unstructured":"Lowe, G.: Testing for linearizability. Concurr. Comput.: Pract. Exp. 29, e3928 (2017)","journal-title":"Concurr. Comput.: Pract. Exp."},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-031-37706-8_8","volume-title":"Computer Aided Verification","author":"N Koval","year":"2023","unstructured":"Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., Alistarh, D.: Lincheck: a practical framework for testing concurrent data structures on JVM. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13964, pp. 156\u2013169. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_8"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-031-35257-7_12","volume-title":"Theoretical Aspects of Software Engineering","author":"Q Jia","year":"2023","unstructured":"Jia, Q., et al.: VeriLin: A linearizability checker for large-scale concurrent objects. In: David, C., Sun, M. (eds.) TASE 2023. LNCS, vol. 13931, pp. 202\u2013220. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35257-7_12"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Emmi, M., Enea, C.: Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang. 2, 25:1\u201325:27 (2018)","DOI":"10.1145\/3158113"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 164\u2013182 (1993)","DOI":"10.1006\/jpdc.1993.1015"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-19195-9_4","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"A Horn","year":"2015","unstructured":"Horn, A., Kroening, D.: Faster linearizability checking via P-compositionality. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 50\u201365. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_4"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: POPL 2013, pp. 459\u2013470 (2013)","DOI":"10.1145\/2491956.2462189"},{"key":"18_CR11","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Technical report, University of Cambridge, Computer Laboratory (2008)"},{"key":"18_CR12","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., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160, 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Klein, G., et\u00a0al.: seL4: formal verification of an OS kernel. In: SOSP 2009, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"18_CR14","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI 2016, pp. 653\u2013669. ACM (2016)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Zou, M., Ding, H., Du, D., Fu, M., Gu, R., Chen, H.: Using concurrent relational logic with helpers for verifying the AtomFS file system. In: SOSP 2019, pp. 259\u2013274. ACM (2019)","DOI":"10.1145\/3341301.3359644"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-25423-4_12","volume-title":"Formal Methods and Software Engineering","author":"J Cui","year":"2015","unstructured":"Cui, J., Duan, Z., Tian, C., Zhang, N., Zhou, C.: Model checking $$\\mu $$C\/OS-III multi-task system with TMSVL. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 187\u2013200. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_12"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1002\/stvr.1482","volume":"24","author":"Y Choi","year":"2014","unstructured":"Choi, Y.: Model checking trampoline OS: a case study on safety analysis for automotive software. Softw. Test. Verif. Reliab. 24, 38\u201360 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"18_CR19","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2020","unstructured":"Herlihy, M., Shavit, N., Luchangco, V., Spear, M.: The Art of Multiprocessor Programming. Newnes, New York (2020)"}],"container-title":["Lecture Notes in Computer Science","Engineering of Complex Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00828-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T04:05:50Z","timestamp":1779768350000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00828-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,17]]},"ISBN":["9783032008275","9783032008282"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00828-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,17]]},"assertion":[{"value":"17 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICECCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Engineering of Complex Computer Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"2 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iceccs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/iceccs2025-hangzhou.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}