{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:36:36Z","timestamp":1764783396992,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,4,10]],"date-time":"2012-04-10T00:00:00Z","timestamp":1334016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,4,10]]},"DOI":"10.1145\/2168836.2168869","type":"proceedings-article","created":{"date-parts":[[2012,4,10]],"date-time":"2012-04-10T12:19:38Z","timestamp":1334060378000},"page":"323-336","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Improving interrupt response time in a verifiable protected microkernel"],"prefix":"10.1145","author":[{"given":"Bernard","family":"Blackham","sequence":"first","affiliation":[{"name":"NICTA and The University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yao","family":"Shi","sequence":"additional","affiliation":[{"name":"NICTA and The University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA and The University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,4,10]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"R1P1 edition","author":"Technical Reference Manual JF-S","year":"2005","unstructured":"ARM1136 JF-S and ARM1136J-S Technical Reference Manual . ARM Ltd . , R1P1 edition , 2005 . ARM1136JF-S and ARM1136J-S Technical Reference Manual. ARM Ltd., R1P1 edition, 2005."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00365393"},{"key":"e_1_3_2_1_3_1","volume-title":"Emb. World Conf.","author":"Baumann Christoph","year":"2010","unstructured":"Christoph Baumann , Bernhard Beckert , Holger Blasum , and Thorsten Bormer . Ingredients of operating system correctness . In Emb. World Conf. , Nuremberg, Germany , Mar 2010 . Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer. Ingredients of operating system correctness. In Emb. World Conf., Nuremberg, Germany, Mar 2010."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1210250.1210262"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103801"},{"volume-title":"Proceedings of IEEE\/IEE Real-Time Embedded Systems Workshop, 2001. Satellite of the IEEE Real-Time Systems Symposium.","author":"Campoy M.","key":"e_1_3_2_1_7_1","unstructured":"M. Campoy , A.P. Ivars , and J.V.B. Mataix . Static use of locking caches in multitask preemptive real-time systems . In Proceedings of IEEE\/IEE Real-Time Embedded Systems Workshop, 2001. Satellite of the IEEE Real-Time Systems Symposium. M. Campoy, A.P. Ivars, and J.V.B. Mataix. Static use of locking caches in multitask preemptive real-time systems. In Proceedings of IEEE\/IEE Real-Time Embedded Systems Workshop, 2001. Satellite of the IEEE Real-Time Systems Symposium."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9119-8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.14"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/121132.121155"},{"key":"e_1_3_2_1_13_1","first-page":"28","volume-title":"1st MIKES","author":"Elkaduwe Dhammika","year":"2007","unstructured":"Dhammika Elkaduwe , Philip Derrin , and Kevin Elphinstone . A memory allocation model for an embedded microkernel . In 1st MIKES , pages 28 -- 34 , Sydney, Australia , Jan 2007 . NICTA. Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. A memory allocation model for an embedded microkernel. In 1st MIKES, pages 28--34, Sydney, Australia, Jan 2007. NICTA."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375603"},{"key":"e_1_3_2_1_15_1","first-page":"101","volume-title":"3rd OSDI","author":"Ford Brian","year":"1999","unstructured":"Brian Ford , Mike Hibler , Jay Lepreau , Roland McGrath , and Patrick Tullmann . Interface and execution models in the Fluke kernel . In 3rd OSDI , pages 101 -- 115 , New Orleans, LA, USA , Feb 1999 . USENIX. Brian Ford, Mike Hibler, Jay Lepreau, Roland McGrath, and Patrick Tullmann. Interface and execution models in the Fluke kernel. In 3rd OSDI, pages 101--115, New Orleans, LA, USA, Feb 1999. USENIX."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034827"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851276.1851282"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1321774.1321802"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/827267.828940"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168633"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224075"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/827272.829139"},{"key":"e_1_3_2_1_27_1","series-title":"LNCS","first-page":"298","volume-title":"Computer Aided Verification","author":"Metzner Alexander","year":"2004","unstructured":"Alexander Metzner . Why model checking can improve WCET analysis . In Rajeev Alur and Doron Peled, editors, Computer Aided Verification , volume 3114 of LNCS , pages 298 -- 301 . Springer-Verlag , 2004 . Alexander Metzner. Why model checking can improve WCET analysis. In Rajeev Alur and Doron Peled, editors, Computer Aided Verification, volume 3114 of LNCS, pages 298--301. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/827272.829141"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/WISES.2008.4623310"},{"key":"e_1_3_2_1_30_1","volume-title":"School Comp. Sci. & Engin.","author":"Warton Matthew","year":"2052","unstructured":"Matthew Warton . Single kernel stack L4. BE thesis , School Comp. Sci. & Engin. , University NSW , Sydney 2052 , Australia, Nov 2005. Matthew Warton. Single kernel stack L4. BE thesis, School Comp. Sci. & Engin., University NSW, Sydney 2052, Australia, Nov 2005."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"}],"event":{"name":"EuroSys '12: Seventh EuroSys Conference 2012","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Bern Switzerland","acronym":"EuroSys '12"},"container-title":["Proceedings of the 7th ACM european conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2168836.2168869","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2168836.2168869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:54:45Z","timestamp":1750240485000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2168836.2168869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,10]]},"references-count":30,"alternative-id":["10.1145\/2168836.2168869","10.1145\/2168836"],"URL":"https:\/\/doi.org\/10.1145\/2168836.2168869","relation":{},"subject":[],"published":{"date-parts":[[2012,4,10]]},"assertion":[{"value":"2012-04-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}