{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:02:37Z","timestamp":1790071357170,"version":"4.0.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319431437","type":"print"},{"value":"9783319431444","type":"electronic"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_4","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T00:24:16Z","timestamp":1470443056000},"page":"52-68","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency"],"prefix":"10.1007","author":[{"given":"June","family":"Andronick","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Corey","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Matichuk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"4_CR1","unstructured":"eChronos model and proofs. \n                      https:\/\/github.com\/echronos\/echronos-proofs"},{"key":"4_CR2","unstructured":"FreeRTOS. \n                      http:\/\/www.freertos.org\/"},{"key":"4_CR3","unstructured":"The eChronos OS. \n                      http:\/\/echronos.systems"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: Workshop on Models for Formal Analysis of Real Systems (MARS) (2015)","DOI":"10.4204\/EPTCS.196.2"},{"key":"4_CR5","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: MEMOCODE, pp. 62\u201371. IEEE (2014)","DOI":"10.1109\/MEMCOD.2014.6961844"},{"issue":"1","key":"4_CR6","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s00165-014-0308-9","volume":"27","author":"S Cheng","year":"2015","unstructured":"Cheng, S., Woodcock, J., D\u2019Souza, D.: Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects Comput. 27(1), 167\u2013192 (2015)","journal-title":"Formal Aspects Comput."},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-25423-4_11","volume-title":"Formal Methods and Software Engineering","author":"S Divakaran","year":"2015","unstructured":"Divakaran, S., D\u2019Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: Refinement-based verification of the FreeRTOS scheduler in VCC. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) Formal Methods and Software Engineering. LNCS, vol. 9047, pp. 170\u2013186. Springer, Heidelberg (2015)"},{"key":"4_CR8","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3126-2","volume-title":"On a Method of Multiprogramming","author":"WHJ Feijen","year":"1999","unstructured":"Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Monographs in Computer Science. Springer, New York (1999)"},{"issue":"2\u20134","key":"4_CR9","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10817-009-9118-9","volume":"42","author":"X Feng","year":"2009","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reasoning 42(2\u20134), 301\u2013347 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"4_CR10","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s10009-014-0307-4","volume":"16","author":"JF Ferreira","year":"2014","unstructured":"Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.N.: Automated verification of the FreeRTOS scheduler in HIP\/SLEEK. Int. J. Softw. Tools Technol. Transf. 16(4), 381\u2013397 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR11","first-page":"11","volume-title":"PLDI 2015: The 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation","author":"P Gammie","year":"2015","unstructured":"Gammie, P., Hosking, T.A., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Blackburn, S. (ed.) PLDI 2015: The 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation, p. 11. ACM, New York (2015)"},{"issue":"4","key":"4_CR12","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1017\/S0956796813000075","volume":"23","author":"A Gotsman","year":"2013","unstructured":"Gotsman, A., Yang, H.: Modular verification of preemptive OS kernels. J. Funct. Program. 23(4), 452\u2013514 (2013)","journal-title":"J. Funct. Program."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Guo, Y., Zhang, H.: Verifying preemptive kernel code with preemption control support. In: 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, 1\u20133 September 2014, pp. 26\u201333. IEEE (2014)","DOI":"10.1109\/TASE.2014.29"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: Theoretical Aspects of Software Engineering (TASE), pp. 142\u2013149. IEEE (2011)","DOI":"10.1109\/TASE.2011.11"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-06410-9_2","volume-title":"FM 2014: Formal Methods","author":"G Klein","year":"2014","unstructured":"Klein, G.: Proof engineering considered essential. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 16\u201321. Springer, Heidelberg (2014)"},{"issue":"1","key":"4_CR16","first-page":"2:1","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. Trans. Comput. Syst. 32(1), 2:1\u20132:70 (2014)","journal-title":"Trans. Comput. Syst."},{"key":"4_CR17","first-page":"53","volume-title":"POPL 2010 WS Declarative Aspects of Multicore Programming","author":"DC Matthews","year":"2010","unstructured":"Matthews, D.C., Wenzel, M.: Efficient parallel programming in Poly\/ML and Isabelle\/ML. In: Petersen, L., Pontelli, E. (eds.) POPL 2010 WS Declarative Aspects of Multicore Programming, pp. 53\u201362. ACM, New York (2010)"},{"key":"4_CR18","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"4_CR20","unstructured":"Prensa Nieto, L.: Verification of parallel programs with the Owicki-Gries and rely-guarantee methods in Isabelle\/HOL. Ph.D. thesis, T.U. M\u00fcnchen (2002)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: 2010 PLDI, pp. 99\u2013110. ACM (2010)","DOI":"10.1145\/1806596.1806610"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:07:01Z","timestamp":1558314421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"7 August 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 August 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}