{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T10:34:51Z","timestamp":1725878091354},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_22","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"405-423","source":"Crossref","is-referenced-by-count":6,"title":["Detecting All High-Level Dataraces in an RTOS Kernel"],"prefix":"10.1007","author":[{"given":"Suvam","family":"Mukherjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arun","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"D\u2019Souza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"issue":"2","key":"22_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1119479.1119480","volume":"28","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: static race detection for Java. ACM Trans. Program. Lang. Syst. (TOPLAS) 28(2), 207\u2013255 (2006)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1\u20132","key":"22_CR2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R Alur","year":"2000","unstructured":"Alur, R., McMillan, K.L., Peled, D.A.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1\u20132), 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"22_CR3","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1002\/stvr.281","volume":"13","author":"C Artho","year":"2003","unstructured":"Artho, C., Havelund, K., Biere, A.: High-level data races. Software Test., Verification & Reliab. 13, 207\u2013227 (2003)","journal-title":"Software Test., Verification & Reliab."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Chandrasekaran, P., Kumar, K.B.S., Minz, R.L., D\u2019Souza, D., Meshram, L.: A multi-core version of FreeRTOS verified for datarace and deadlock freedom. In: Proceedings of ACM\/IEEE Formal Methods and Models for Codesign (MEMOCODE), pp. 62\u201371 (2014)","DOI":"10.1109\/MEMCOD.2014.6961844"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Choi, J.-D., Lee, K., Loginov, A., O\u2019Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: Proceedings of ACM SIGPLAN Programming Languages Design and Implementation (PLDI), pp. 258\u2013269. ACM, New York (2002)","DOI":"10.1145\/512529.512560"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-39611-3_8","volume-title":"Hardware and Software: Verification and Testing","author":"RJ Dias","year":"2013","unstructured":"Dias, R.J., Pessanha, V., Louren\u00e7o, J.M.: Precise detection of atomicity violations. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 8\u201323. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_8"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Dinning, A., Schonberg, E.: Detecting access anomalies in programs with critical sections. In: Proceedings of ACM\/ONR Workshop on Parallel and Distributed Debugging (PADD), pp. 85\u201396. ACM, New York (1991)","DOI":"10.1145\/122759.122767"},{"key":"22_CR8","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Precise race detection and efficient model checking using locksets. Technical Report MSR-TR\u2013118, Microsoft Research (2005)"},{"issue":"5","key":"22_CR9","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/1165389.945468","volume":"37","author":"D Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. SIGOPS Oper. Syst. Rev. 37(5), 237\u2013252 (2003)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"22_CR10","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"},{"issue":"2","key":"22_CR11","doi-asserted-by":"crossref","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."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Fasttrack: Efficient and precise dynamic race detection. In: Proceedings of ACM SIGPLAN PLDI, pp. 121\u2013133. ACM, New York (2009)","DOI":"10.1145\/1542476.1542490"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 338\u2013349 (2003)","DOI":"10.1145\/781131.781169"},{"issue":"8","key":"22_CR14","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749\u2013765 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-48234-2_17","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K Havelund","year":"1999","unstructured":"Havelund, K., Skakkeb\u00e6k, J.U.: Applying model checking in Java verification. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 216\u2013231. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48234-2_17"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 1\u201313 (2004)","DOI":"10.1145\/996841.996844"},{"issue":"3","key":"22_CR17","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23, 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Sinha, N., Kruus, E., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: ACM SIGSOFT FSE, pp. 13\u201322. ACM, New York (2009)","DOI":"10.1145\/1595696.1595701"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Proceedings of Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 37\u201348 (2006)","DOI":"10.1145\/1168857.1168864"},{"key":"22_CR21","unstructured":"Mukherjee, S., Arunkumar, S., D\u2019Souza, D.: Proving an RTOS kernel free of data-races. Technical Report CSA-TR-2016-1, Department of Computer Science and Automation, IISc (2016)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Proceedings of ACM SIG-PLAN Programming Languages Design and Implementaion (PLDI), pp. 14\u201324 (2004)","DOI":"10.1145\/996841.996845"},{"key":"22_CR23","unstructured":"Real Time Engineers Ltd., The FreeRTOS Real Time Operating System (2014)"},{"issue":"4","key":"22_CR24","doi-asserted-by":"crossref","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. (TOCS) 15(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-54013-4_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"MD Schwarz","year":"2014","unstructured":"Schwarz, M.D., Seidl, H., Vojdani, V., Apinis, K.: Precise analysis of value-dependent synchronization in priority scheduled programs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 21\u201338. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54013-4_2"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., M\u00fcller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: Proceedings ACM SIGPLAN-SIGACT Principles of Programming Languages (POPL), pp. 93\u2013104 (2011)","DOI":"10.1145\/1926385.1926398"},{"key":"22_CR27","unstructured":"Sterling, N.: WARLOCK - a static data race analysis tool. In: Proceedings of Usenix Winter Technical Conference, pp. 97\u2013106 (1993)"},{"issue":"6","key":"22_CR28","doi-asserted-by":"crossref","first-page":"103","DOI":"10.5381\/jot.2004.3.6.a5","volume":"3","author":"C Praun von","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."},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Voung, J. W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Proceedings of ESEC\/SIGSOFT Foundation of Software Engineering (FSE), pp. 205\u2013214 (2007)","DOI":"10.1145\/1287624.1287654"},{"issue":"2","key":"22_CR30","doi-asserted-by":"crossref","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":"22_CR31","doi-asserted-by":"crossref","unstructured":"Xu, M., Bod\u00edk, R., Hill, M.D.: A serializability violation detector for shared-memory server programs. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 1\u201314 (2005)","DOI":"10.1145\/1065010.1065013"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-31759-0_14","volume-title":"Model Checking Software","author":"R Zeng","year":"2012","unstructured":"Zeng, R., Sun, Z., Liu, S., He, X.: McPatom: a predictive analysis tool for atomicity violation using model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 191\u2013207. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31759-0_14"}],"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-319-52234-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T03:53:56Z","timestamp":1498362836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}