{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:27Z","timestamp":1770896187695,"version":"3.50.1"},"reference-count":80,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,7,27]],"date-time":"2017-07-27T00:00:00Z","timestamp":1501113600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,7,27]],"date-time":"2017-07-27T00:00:00Z","timestamp":1501113600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-9-0179"],"award-info":[{"award-number":["FA8750-12-9-0179"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Real-Time Syst"],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1007\/s11241-017-9286-3","type":"journal-article","created":{"date-parts":[[2017,7,27]],"date-time":"2017-07-27T19:48:27Z","timestamp":1501184907000},"page":"812-853","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["High-assurance timing analysis for a high-assurance real-time operating system"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4891-0797","authenticated-orcid":false,"given":"Thomas","family":"Sewell","sequence":"first","affiliation":[]},{"given":"Felix","family":"Kam","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,27]]},"reference":[{"key":"9286_CR1","unstructured":"Amadio RM, Ayache N, Bobot F, Boender JP, Campbell B, Garnier I, Madet A, McKinna J, Mulligan DP, Piccolo M, et\u00a0al Certified complexity (CerCo) (2013) In: International workshop on foundational and practical aspects of resource analysis. Springer, Berlin, pp 1\u201318"},{"key":"9286_CR2","doi-asserted-by":"crossref","unstructured":"Ayache N, Amadio R, R\u00e9gis-Gianas Y (2012) Certifying and reasoning on cost annotations in C programs. In: FMICS 2012\u201417th international workshop on formal methods for industrial critical systems, Paris, France, Aug 2012","DOI":"10.1007\/978-3-642-32469-7_3"},{"key":"9286_CR3","doi-asserted-by":"crossref","unstructured":"Andronick J, Lewis C, Morgan C (2015) Controlled owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: van Glabbeek RJ, Groote JF, H\u00f6fner P (eds) Workshop on models for formal analysis of real systems (MARS 2015), Suva, Fiji, pp 10\u201324, Nov 2015","DOI":"10.4204\/EPTCS.196.2"},{"key":"9286_CR4","unstructured":"Alkassar E, Paul W, Starostin A, Tsyban A (2010) Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In: O\u2019Hearn P, Leavens GT, Rajamani S (eds) VSTTE 2010. LNCS, vol 6217, Edinburgh, UK. Springer, pp 71\u201385, Aug 2010"},{"key":"9286_CR5","unstructured":"Avionics Application Software Standard Interface (2012) ARINC Standard 653"},{"key":"9286_CR6","unstructured":"Barhorst J, Belote T, Binns P, Hoffman J, Paunicka J, Sarathy P, Scoredos J, Stanfill P, Stuart D, Urzi R (2009) A research agenda for mixed-criticality systems. \n                    http:\/\/www.cse.wustl.edu\/~cdgill\/CPSWEEK09_MCAR\/"},{"issue":"11","key":"9286_CR7","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"WR Bevier","year":"1989","unstructured":"Bevier WR (1989) Kit: a study in operating system verification. Trans Softw Eng 15(11):1382\u20131396","journal-title":"Trans Softw Eng"},{"key":"9286_CR8","unstructured":"Bromberger AC, Peri Frantz A, Frantz WS, Hardy AC, Hardy N, Landau CR, Shapiro JS (1992) The KeyKOS nanokernel architecture. In: USENIX WS Microkernels & other Kernel Arch. Seattle, WA, US, pp 95\u2013112"},{"key":"#cr-split#-9286_CR9.1","doi-asserted-by":"crossref","unstructured":"Blackham B, Heiser G (2013) Sequoll: a framework for model checking binaries. In: Tovar E","DOI":"10.1109\/RTAS.2013.6531083"},{"key":"#cr-split#-9286_CR9.2","unstructured":"(ed) RTAS, Philadelphia, USA, pp 97-106, Apr 2013"},{"key":"9286_CR10","doi-asserted-by":"crossref","unstructured":"Blanc R, Henzinger TA, Hottelier T, Kov\u00e1cs L (2010) ABC: algebraic bound computation for loops. In: 16th international conference on logic programming, artificial intelligence & reasoning. Springer, pp 103\u2013118","DOI":"10.1007\/978-3-642-17511-4_7"},{"key":"9286_CR11","doi-asserted-by":"crossref","unstructured":"Bardin S, Herrmann P, V\u00e9drine F (2011) Refinement-based CFG reconstruction from unstructured programs. In: International conference on verification, model checking & abstract interpretation. Springer, Berlin, pp 54\u201369","DOI":"10.1007\/978-3-642-18275-4_6"},{"key":"#cr-split#-9286_CR12.1","doi-asserted-by":"crossref","unstructured":"Blackham B, Liffiton M, Heiser G (2014) Trickle: automated infeasible path detection using all minimal unsatisfiable subsets. In: West R","DOI":"10.1109\/RTAS.2014.6926000"},{"key":"#cr-split#-9286_CR12.2","unstructured":"(ed) RTAS, Berlin, Germany, pp 169-178, Apr 2014"},{"key":"9286_CR13","unstructured":"Burgui\u00e8re C, Rochange C (2006) History-based schemes and implicit path enumeration. In: 6th WS worst-case execution-time analysis"},{"key":"9286_CR14","doi-asserted-by":"crossref","unstructured":"Blackham B, Shi Y, Chattopadhyay S, Roychoudhury A, Heiser G (2011) Timing analysis of a protected operating system kernel. In: RTSS, Vienna, Austria, pp 339\u2013348, Nov 2011","DOI":"10.1109\/RTSS.2011.38"},{"key":"9286_CR15","doi-asserted-by":"crossref","unstructured":"Blackham B, Shi Y, Heiser G (2012) Improving interrupt response time in a verifiable protected microkernel. In: EuroSys, Bern, Switzerland, pp 323\u2013336, Apr 2012","DOI":"10.1145\/2168836.2168869"},{"key":"9286_CR16","doi-asserted-by":"crossref","unstructured":"Blackham B, Tang V, Heiser G (2012) To preempt or not to preempt, that is the question. In: APSys, ACM, Seoul, Korea, p 7, July 2012","DOI":"10.1145\/2349896.2349904"},{"issue":"5","key":"9286_CR17","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Yuan L, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"9286_CR18","unstructured":"Cullmann C, Martin F (2007) Data-flow based detection of loop bounds. In: 7th WS worst-case execution-time analysis"},{"key":"9286_CR19","doi-asserted-by":"crossref","unstructured":"Cohen E, Schirmer N (2010) From total store order to sequential consistency: a practical reduction theorem. In: Kaufmann M, Paulson L (eds) 1st ITP. LNCS, vol 6172. Springer, Edinburgh, UK, pp 403\u2013418, July 2010","DOI":"10.1007\/978-3-642-14052-5_28"},{"key":"9286_CR20","unstructured":"Dietz W, Li P, Regehr J, Adve V (2012) Understanding integer overflow in C\/C++. In: Proceedings of the 34th international conference on software engineering, ICSE \u201912. IEEE Press, Piscataway, NJ, USA, pp 760\u2013770"},{"key":"9286_CR21","unstructured":"de\u00a0Roever WP, de\u00a0Boer F, Hanneman U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and non-compositional methods. Cambridge Tracts in Theoretical Computer Science"},{"key":"9286_CR22","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/365230.365252","volume":"9","author":"JB Dennis","year":"1966","unstructured":"Dennis JB, Van Horn EC (1966) Programming semantics for multiprogrammed computations. CACM 9:143\u2013155","journal-title":"CACM"},{"key":"9286_CR23","unstructured":"Ermedahl A, Sandberg C, Gustafsson J, Bygde S, Lisper B (2007) Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: WS worst-case execution-time analysis"},{"key":"9286_CR24","doi-asserted-by":"crossref","unstructured":"Feng X, Ferreira R, Shao Z (2007) On the relationship between concurrent separation logic and assume-guarantee reasoning. In: ESOP. Springer, pp 173\u2013188","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"9286_CR25","doi-asserted-by":"crossref","unstructured":"Ferdinand C, Heckmann R, Langenbach M, Martin F, Schmidt M, Theiling H, Thesing S, Wilhelm R (2001) Reliable and precise WCET determination for a real-life processor. In: EMSOFT. Springer, London, UK, pp 469\u2013485","DOI":"10.1007\/3-540-45449-7_32"},{"key":"9286_CR26","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd RW (1967) Assigning meanings to programs. Math Asp Comput Sci 19:19\u201332","journal-title":"Math Asp Comput Sci"},{"key":"9286_CR27","doi-asserted-by":"crossref","unstructured":"Fox A, Myreen M (2010) A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann M, Paulson LC (eds) 1st ITP. LNCS, vol 6172. Springer, Edinburgh, UK, pp 243\u2013258, July 2010","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"9286_CR28","unstructured":"Gustafsson J, Betts A, Ermedahl A, Lisper B (2010) The M\u00e4lardalen WCET benchmarks\u2014past, present and future. In: 10th WS worst-case execution-time analysis. OCG, Brussels, BE, pp 137\u2013147, July 2010"},{"key":"9286_CR29","doi-asserted-by":"crossref","unstructured":"Gustafsson J, Ermedahl A, Sandberg C, Lisper B (2006) Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution. In: RTSS. IEEE Computer Society, Washington, DC, US, pp 57\u201366","DOI":"10.1109\/RTSS.2006.12"},{"key":"9286_CR30","doi-asserted-by":"crossref","unstructured":"Gammie P, Hosking T, Engelhardt K (2015) 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. ACM, Portland, Oregon, United States, p 11, June 2015","DOI":"10.1145\/2737924.2738006"},{"key":"9286_CR31","unstructured":"Gu R, Shao Z, Chen H, Wu X, Kim J, Sj\u00f6berg V, Costanzo D (2016) An extensible architecture for building certified concurrent OS kernels. In: OSDI, CertiKOS"},{"key":"9286_CR32","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/12.743411","volume":"48","author":"CA Healy","year":"1999","unstructured":"Healy CA, Arnold RD, M\u00fcller F, Whalley DB, Harmon Marion G (1999) Bounding pipeline and instruction cache performance. Trans Comput 48:63\u201370","journal-title":"Trans Comput"},{"issue":"1","key":"9286_CR33","first-page":"1:1","volume":"34","author":"G Heiser","year":"2016","unstructured":"Heiser G, Elphinstone K (2016) L4 microkernels: the lessons from 20 years of research and deployment. Trans Comput Syst 34(1):1:1\u20131:29","journal-title":"Trans Comput Syst"},{"key":"9286_CR34","unstructured":"Hergenhan A, Heiser G (2008) Operating systems technology for converged ECUs. In: 6th embedded security in cars conference (escar), Hamburg, Germany, Nov 2008"},{"key":"9286_CR35","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R (2003) Counterexample-guided control. In: 30th ICALP, Eindhoven, The Netherlands, pp 886\u2013902, July 2003","DOI":"10.1007\/3-540-45061-0_69"},{"key":"9286_CR36","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. CACM 12:576\u2013580","journal-title":"CACM"},{"key":"9286_CR37","unstructured":"ISO (2011) ISO26262: road vehicles\u2014functional safety"},{"issue":"1","key":"9286_CR38","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 (2014) Comprehensive formal verification of an OS microkernel. Trans Comput Syst 32(1):2:1\u20132:70","journal-title":"Trans Comput Syst"},{"issue":"1","key":"9286_CR39","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1002\/stvr.406","volume":"20","author":"TH Kim","year":"2010","unstructured":"Kim TH, Bang HJ, Cha SD (2010) A systematic representation of path constraints for implicit path enumeration technique. Softw Test Verif Reliab 20(1):39\u201361","journal-title":"Softw Test Verif Reliab"},{"key":"9286_CR40","doi-asserted-by":"crossref","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J et\u00a0al (2009) seL4: formal verification of an OS kernel. In: SOSP, Big Sky, MT, US, pp 207\u2013220, Oct 2009","DOI":"10.1145\/1629575.1629596"},{"issue":"3","key":"9286_CR41","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/s10270-010-0161-0","volume":"10","author":"R Kirner","year":"2011","unstructured":"Kirner R, Knoop J, Prantl A, Schordan M, Kadlec A (2011) Beyond loop bounds: comparing annotation languages for worst-case execution time analysis. Softw Syst Model 10(3):411\u2013437","journal-title":"Softw Syst Model"},{"key":"9286_CR42","doi-asserted-by":"crossref","unstructured":"Knoop J, Kov\u00e1cs L, Zwirchmayr J (2011) Symbolic loop bound computation for WCET analysis. In: International Andrei Ershov memorial conference","DOI":"10.1007\/978-3-642-29709-0_20"},{"key":"9286_CR43","doi-asserted-by":"crossref","unstructured":"Knoop J, Kov\u00e1cs L, Zwirchmayr J (2013) WCET squeezing: On-demand feasibility refinement for proven precise WCET-bounds. In: Proceedings of the 21st international conference on real-time networks and systems, RTNS \u201913. ACM, New York, NY, USA, pp 161\u2013170","DOI":"10.1145\/2516821.2516847"},{"issue":"1","key":"9286_CR44","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G Klein","year":"2009","unstructured":"Klein G (2009) Operating system verification\u2014an overview. S\u0101dhan\u0101 34(1):27\u201369","journal-title":"S\u0101dhan\u0101"},{"key":"9286_CR45","unstructured":"Kinder J, Zuleger F, Veith H (2009) An abstract interpretation-based framework for control flow reconstruction from binaries. In: 10th International conference on verification, model checking & abstract interpretation. Springer, pp 214\u2013228"},{"key":"9286_CR46","unstructured":"Lokuciejewski P, Cordes D, Falk H, Marwedel P (2009) A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models. In: 7th symposium code generation & optimization. IEEE Computer Society, Washington, DC, US, pp 136\u2013146"},{"issue":"7","key":"9286_CR47","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. CACM 52(7):107\u2013115","journal-title":"CACM"},{"key":"9286_CR48","unstructured":"Lyons A, Heiser G (2014) Mixed-criticality support in a high-assurance, general-purpose microkernel. In: Davis R, Cucu-Grosjean L (eds) WS mixed criticality system, Rome, Italy, pp 9\u201314, Dec 2014"},{"key":"9286_CR49","unstructured":"Lyons A, Heiser G (2016) It\u2019s time: OS mechanisms for enforcing asymmetric temporal integrity. arXiv preprint"},{"key":"9286_CR50","unstructured":"Liedtke J (1994) Page table structures for fine-grain virtual memory. In: IEEE Technical Committee on Computer Architecture Newsletter, Oct 1994"},{"key":"9286_CR51","unstructured":"Lisper B (2005) Ideas for annotation language (s). Technical report, Technical Report Oct. 25, Department of Computer Science and Engineering, University of M\u00e4lardalen"},{"issue":"1\u20133","key":"9286_CR52","first-page":"56","volume":"69","author":"X Li","year":"2007","unstructured":"Li X, Liang Y, Mitra T, Roychoudhury A (2007) Chronos: a timing analyzer for embedded software. Sci Comput Program Spec Issue Exp Softw Toolkit 69(1\u20133):56\u201367","journal-title":"Sci Comput Program Spec Issue Exp Softw Toolkit"},{"key":"9286_CR53","unstructured":"Li Y-T, Malik S (1995) Performance analysis of embedded software using implicit path enumeration. In: Proceedings of the 32nd ACM\/IEEE design automation conference. ACM, pp 456\u2013461, June 1995"},{"key":"9286_CR54","doi-asserted-by":"crossref","unstructured":"Lundqvist T, Stenstr\u00f6m P (1998) Integrating path and timing analysis using instruction level simulation techniques. In: Proceedings of the ACM SIGPLAN workshop on languages, compilers and tools for embedded systems. LNCS. Springer, Montreal CA, June 1998","DOI":"10.1007\/BFb0057776"},{"key":"9286_CR55","unstructured":"Li Y, West R, Missimer ES (2013) The quest-V separation kernel for mixed criticality systems. In: WS mixed criticality system, pp 31\u201336, Dec 2013"},{"key":"9286_CR56","unstructured":"MISRA (2012) Guidelines for the Use of the C language in critical systems"},{"key":"9286_CR57","doi-asserted-by":"crossref","unstructured":"Murray T, Matichuk D, Brassil M, Gammie P, Bourke T, Seefried S, Lewis C, Gao X, Klein G (2013) seL4: from general purpose to a proof of information flow enforcement. In: S&P, San Francisco, CA, pp 415\u2013429, May 2013","DOI":"10.1109\/SP.2013.35"},{"issue":"3","key":"9286_CR58","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1016324624000","volume":"9","author":"WB Martin","year":"2002","unstructured":"Martin WB, White PD, Taylor FS (2002) Creating high confidence in a separation kernel. Autom Softw Eng 9(3):263\u2013284","journal-title":"Autom Softw Eng"},{"key":"9286_CR59","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson L, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. LNCS, vol 2283. Springer, Berlin","DOI":"10.1007\/3-540-45949-9"},{"issue":"2","key":"9286_CR60","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BF00571421","volume":"1","author":"P Puschner","year":"1989","unstructured":"Puschner P, Koza C (1989) Calculating the maximum execution time of real-time programs. Real-Time Syst 1(2):159\u2013176","journal-title":"Real-Time Syst"},{"key":"9286_CR61","unstructured":"Prantl A, Knoop J, Kirner R, Kadlec A, Schordan M (2009) From trusted annotations to verified knowledge. In: WS worst-case execution-time analysis, Dublin, IE, pp 35\u201345, June 2009"},{"issue":"5","key":"9286_CR62","first-page":"48","volume":"24","author":"CY Park","year":"1991","unstructured":"Park CY, Shaw AC (1991) Experiments with a program timing tool based on source\u2013level timing schema. Trans Comput 24(5):48\u201357","journal-title":"Trans Comput"},{"key":"9286_CR63","doi-asserted-by":"crossref","unstructured":"Raymond P (2014) A general approach for expressing infeasibility in implicit path enumeration technique. In: Proceedings of the 14th international conference on embedded software. ACM, pp 8","DOI":"10.1145\/2656045.2656046"},{"key":"9286_CR64","doi-asserted-by":"crossref","unstructured":"Rieder B, Puschner P, Wenzel I (2008) Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis. In: 2008 International Workshop on intelligent solutions in embedded systems, pp 1\u20137, Jul 2008","DOI":"10.1109\/WISES.2008.4623310"},{"key":"9286_CR65","unstructured":"RTCA (1992) DO-178B: Software Considerations in Airborne Systems and Equipment Certification"},{"key":"9286_CR66","unstructured":"RTCA (2011) DO-178C: Software Considerations in Airborne Systems and Equipment Certification"},{"key":"9286_CR67","doi-asserted-by":"crossref","unstructured":"Rushby J (1981) Design and verification of secure systems. In: SOSP, Pacific Grove, CA, USA, pp 12\u201321, Dec 1981","DOI":"10.1145\/800216.806586"},{"key":"9286_CR68","doi-asserted-by":"crossref","unstructured":"Shi Y, Blackham B, Heiser G (2013) Code optimizations using formally verified properties. In: OOPSLA, Indianapolis, USA, pp 427\u2013442, Oct 2013","DOI":"10.1145\/2509136.2509513"},{"issue":"4","key":"9286_CR69","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1721695.1721702","volume":"9","author":"B Schlich","year":"2010","unstructured":"Schlich B (2010) Model checking of software for microcontrollers. ACM Trans Embed Comput Syst 9(4):36","journal-title":"ACM Trans Embed Comput Syst"},{"key":"9286_CR70","doi-asserted-by":"crossref","unstructured":"Sewell T, Myreen M, Klein G (2013) Translation validation for a verified OS kernel. In: PLDI. ACM, Seattle, Washington, USA, pp 471\u2013481, Jun 2013","DOI":"10.1145\/2491956.2462183"},{"key":"9286_CR71","doi-asserted-by":"crossref","unstructured":"Slind K, Norrish M (2008) A brief overview of HOL4. In: Mohamed OA, Muoz C, Tahar S (eds) TPHOLs. Springer, Montral, Canada, pp 28\u201332, Aug 2008","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"9286_CR72","doi-asserted-by":"crossref","unstructured":"Sewell T, Winwood S, Gammie P, Murray T, Andronick J, Klein G (2011) seL4 enforces integrity. In: van Eekelen M, Geuvers H, Schmaltz J, Wiedijk F (eds) ITP. Springer, Nijmegen, The Netherlands, pp 325\u2013340, Aug 2011","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"9286_CR73","doi-asserted-by":"crossref","unstructured":"Tuch H, Klein G, Norrish M (2007) Types, bytes, and separation logic. In: Hofmann M, Felleisen M (eds) POPL. ACM, Nice, France, pp 97\u2013108, Jan 2007","DOI":"10.1145\/1190216.1190234"},{"key":"9286_CR74","doi-asserted-by":"crossref","unstructured":"Turon A, Vafeiadis V, Dreyer D (2014) GPS: navigating weak memory with ghosts, protocols, and separation. In: ACM SIGPLAN notices, vol 49. ACM, pp 691\u2013707","DOI":"10.1145\/2714064.2660243"},{"key":"9286_CR75","unstructured":"US National Institute of Standards (1999) Common criteria for IT security evaluation. ISO Standard 15408. \n                    http:\/\/csrc.nist.gov\/cc\/"},{"issue":"3","key":"9286_CR76","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R Wilhelm","year":"2008","unstructured":"Wilhelm R, Engblom J, Ermedahl A, Holsti N, Thesing S, Whalley D, Bernat G, Ferdinand C, Heckmann R, Mitra Tulika, Mueller Frank, Puaut I, Puschner P, Staschulat J, Stenstr\u00f6m P (2008) The worst-case execution-time problem\u2014overview of methods and survey of tools. Trans Embed Comput Syst 7(3):1\u201353","journal-title":"Trans Embed Comput Syst"},{"issue":"2","key":"9286_CR77","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"BJ Walker","year":"1980","unstructured":"Walker BJ, Kemmerer RA, Popek GJ (1980) Specification and verification of the UCLA Unix security kernel. CACM 23(2):118\u2013131","journal-title":"CACM"},{"key":"9286_CR78","doi-asserted-by":"crossref","unstructured":"Yang J, Hawblitzel C (2010) Safe to the last instruction: automated verification of a type-safe operating system. In: 2010 PLDI. ACM, Toronto, Ont, CA, pp 99\u2013110, Jun 2010","DOI":"10.1145\/1806596.1806610"}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11241-017-9286-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-017-9286-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-017-9286-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T14:04:45Z","timestamp":1589724285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11241-017-9286-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,27]]},"references-count":80,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["9286"],"URL":"https:\/\/doi.org\/10.1007\/s11241-017-9286-3","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"value":"0922-6443","type":"print"},{"value":"1573-1383","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,27]]},"assertion":[{"value":"27 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}