{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:38:40Z","timestamp":1742978320974,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_26","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"417-432","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder"],"prefix":"10.1007","author":[{"given":"Saurabh","family":"Gadia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cyrille","family":"Artho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gedare","family":"Bloom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"26_CR1","unstructured":"RTEMS real time operating system (RTOS) (2016). https:\/\/www.rtems.org\/"},{"key":"26_CR2","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-642-15234-4_10","volume-title":"Distributed, Parallel and Biologically Inspired Systems","author":"C Artho","year":"2010","unstructured":"Artho, C., Hagiya, M., Leungwattanakit, W., Tanabe, Y., Yamamoto, M.: Model checking of concurrent algorithms: from Java to C. In: Hinchey, M., Kleinjohann, B., Kleinjohann, L., Lindsay, P.A., Rammig, F.J., Timmis, J., Wolf, M. (eds.) DIPES 2010. IFIP AICT, vol. 329, pp. 90\u2013101. Springer, Heidelberg (2010)"},{"issue":"1","key":"26_CR3","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E Clarke","year":"1996","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"26_CR4","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"26_CR5","unstructured":"Gadhia, S., Artho, C., Ramirez, D.: Model locks with thread priority from RTEMS (2015). https:\/\/github.com\/saurabhgadia4\/lock-model"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"26_CR7","volume-title":"The SPIN Model Checker","author":"G Holzmann","year":"2004","unstructured":"Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2004)"},{"issue":"1","key":"26_CR8","doi-asserted-by":"crossref","first-page":"2:1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1\u20132:70 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"26_CR9","volume-title":"Concurrent Programming in Java","author":"D Lea","year":"1999","unstructured":"Lea, D.: Concurrent Programming in Java, 2nd edn. Addison-Wesley, Reading (1999)","edition":"2"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/11562948_33","volume-title":"Automated Technology for Verification and Analysis","author":"G Lindstrom","year":"2005","unstructured":"Lindstrom, G., Mehlitz, P.C., Visser, W.: Model checking real time Java using Java PathFinder. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 444\u2013456. Springer, Heidelberg (2005)"},{"key":"26_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Springer, Heidelberg (1993)"},{"key":"26_CR12","volume-title":"Pthreads Programming","author":"B Nichols","year":"1998","unstructured":"Nichols, B., Buttlar, D., Farrell, J.: Pthreads Programming. O\u2019Reilly, Beijing (1998)"},{"key":"26_CR13","series-title":"LNCS","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: IEEE Proceedings of 17th Annual Symposium on Foundations of Computer Science (FOCS), Rhode Island, USA, pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"9","key":"26_CR15","doi-asserted-by":"crossref","first-page":"1175","DOI":"10.1109\/12.57058","volume":"39","author":"L Sha","year":"1990","unstructured":"Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority inheritance protocols: an approach to real-time synchronization. IEEE Trans. Comput. 39(9), 1175\u20131185 (1990)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"26_CR16","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. J. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng. J."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T21:08:04Z","timestamp":1498338484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}