{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:45:41Z","timestamp":1775054741668,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030304454","type":"print"},{"value":"9783030304461","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-30446-1_17","type":"book-chapter","created":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:03:18Z","timestamp":1567969398000},"page":"315-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Efficient Formal Verification for the Linux Kernel"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4577-7855","authenticated-orcid":false,"given":"Daniel Bristot","family":"de Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0362-0657","authenticated-orcid":false,"given":"Tommaso","family":"Cucinotta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8853-9021","authenticated-orcid":false,"given":"R\u00f4mulo Silva","family":"de Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,9]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Akesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica - an integrated environment for verification, synthesis and simulation of discrete event systems. In: 2006 8th International Workshop on Discrete Event Systems, pp. 384\u2013385, July 2006. https:\/\/doi.org\/10.1109\/WODES.2006.382401","DOI":"10.1109\/WODES.2006.382401"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: concurrency in the Linux Kernel. In: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2018, pp. 405\u2013418. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3173162.3177156","DOI":"10.1145\/3173162.3177156"},{"key":"17_CR3","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Technical Report MSR-TR-2004-08 - SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft - Microsoft Research, January 2004. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/tr-2004-08.pdf"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 1\u20133. ACM, New York (2002). https:\/\/doi.org\/10.1145\/503272.503274","DOI":"10.1145\/503272.503274"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-28756-5_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Basler","year":"2012","unstructured":"Basler, G., Donaldson, A., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: satabs: a bit-precise verifier for C programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 552\u2013555. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_47"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Blackham, B., Shi, Y., Chattopadhyay, S., Roychoudhury, A., Heiser, G.: Timing analysis of a protected operating system kernel. In: Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS11), Vienna, Austria, pp. 339\u2013348, November 2011","DOI":"10.1109\/RTSS.2011.38"},{"key":"17_CR7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2010","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2010)","edition":"2"},{"issue":"6","key":"17_CR8","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388\u2013402 (2004). https:\/\/doi.org\/10.1109\/TSE.2004.22","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s00165-005-0071-z","volume":"17","author":"S Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects Comput. 17(4), 461\u2013483 (2005). https:\/\/doi.org\/10.1007\/s00165-005-0071-z","journal-title":"Formal Aspects Comput."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Chishiro, H.: RT-Seed: real-time middleware for semi-fixed-priority scheduling. In: 2016 IEEE 19th International Symposium on Real-Time Distributed Computing (ISORC) (2016)","DOI":"10.1109\/ISORC.2016.26"},{"key":"17_CR11","unstructured":"Condliffe, J.: U.S. military drones are going to start running on Linux, July 2014. https:\/\/gizmodo.com\/u-s-military-drones-are-going-to-start-running-on-linu-1572853572"},{"key":"17_CR12","unstructured":"Corbet, J.: The kernel lock validator, May 2006. https:\/\/lwn.net\/Articles\/185666\/"},{"key":"17_CR13","unstructured":"Corbet, J.: Linux at NASDAQ OMX, October 2010. https:\/\/lwn.net\/Articles\/411064\/"},{"key":"17_CR14","unstructured":"Corbet, J.: Jump label, October 2010. https:\/\/lwn.net\/Articles\/412072\/"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-24270-0_16","volume-title":"Computer Safety, Reliability, and Security","author":"D Cotroneo","year":"2011","unstructured":"Cotroneo, D., Di Leo, D., Natella, R., Pietrantuono, R.: A case study on state-based robustness testing of an operating system for the avionic domain. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 213\u2013227. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24270-0_16"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Cotroneo, D., Leo, D.D., Fucci, F., Natella, R.: SABRINE: state-based robustness testing of operating systems. In: Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2013, Piscataway, NJ, USA, pp. 125\u2013135. IEEE Press (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693073","DOI":"10.1109\/ASE.2013.6693073"},{"issue":"3","key":"17_CR17","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1109\/TII.2009.2027013","volume":"5","author":"T Cucinotta","year":"2009","unstructured":"Cucinotta, T., et al.: A real-time service-oriented architecture for industrial automation. IEEE Trans. Ind. Inform. 5(3), 267\u2013277 (2009). https:\/\/doi.org\/10.1109\/TII.2009.2027013","journal-title":"IEEE Trans. Ind. Inform."},{"key":"17_CR18","unstructured":"Dronamraju, S.: Linux kernel documentation - uprobe-tracer: Uprobe-based event tracing, May 2019. https:\/\/www.kernel.org\/doc\/Documentation\/trace\/uprobetracer.txt"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Dubey, A., Karsai, G., Abdelwahed, S.: Compensating for timing jitter in computing systems with general-purpose operating systems. In: 2009 IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing, pp. 55\u201362, March 2009. https:\/\/doi.org\/10.1109\/ISORC.2009.28","DOI":"10.1109\/ISORC.2009.28"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-45848-4_57","volume-title":"Graph Drawing","author":"J Ellson","year":"2002","unstructured":"Ellson, J., Gansner, E., Koutsofios, L., North, S.C., Woodhull, G.: Graphviz\u2014open source graph drawing tools. In: Mutzel, P., J\u00fcnger, M., Leipert, S. (eds.) GD 2001. LNCS, vol. 2265, pp. 483\u2013484. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45848-4_57"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 58\u201370. ACM, New York (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"17_CR22","unstructured":"Hiramatsu, M.: Linux tracing technologies: Kprobe-based event tracing, May 2019. https:\/\/www.kernel.org\/doc\/html\/latest\/trace\/kprobetrace.html"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an OS Kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207\u2013220. ACM, New York (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"issue":"3","key":"17_CR25","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.entcs.2009.12.037","volume":"260","author":"B Lei","year":"2010","unstructured":"Lei, B., Liu, Z., Morisset, C., Li, X.: State based robustness testing for components. Electron. Notes Theoret. Comput. Sci. 260, 173\u2013188 (2010). https:\/\/doi.org\/10.1016\/j.entcs.2009.12.037","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"17_CR27","unstructured":"Linux Kernel Documentation: Linux tracing technologies, May 2019. https:\/\/www.kernel.org\/doc\/html\/latest\/trace\/index.html"},{"key":"17_CR28","unstructured":"Marinas, C.: Formal methods for kernel hackers (2018). https:\/\/linuxplumbersconf.org\/event\/2\/contributions\/60\/attachments\/18\/42\/FormalMethodsPlumbers2018.pdf"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Matni, G., Dagenais, M.: Automata-based approach for kernel trace analysis. In: 2009 Canadian Conference on Electrical and Computer Engineering, pp. 970\u2013973, May 2009. https:\/\/doi.org\/10.1109\/CCECE.2009.5090273","DOI":"10.1109\/CCECE.2009.5090273"},{"key":"17_CR30","unstructured":"de Oliveira, D.B.: How can we catch problems that can break the preempt $$\\_$$ rt preemption model? November 2018. https:\/\/linuxplumbersconf.org\/event\/2\/contributions\/190\/"},{"key":"17_CR31","unstructured":"de Oliveira, D.B.: Mind the gap between real-time linux and real-time theory, November 2018. https:\/\/www.linuxplumbersconf.org\/event\/2\/contributions\/75\/"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"de Oliveira, D.B.: Companion page: Efficient formal verification for the linux kernel, May 2019. http:\/\/bristot.me\/efficient-formal-verification-for-the-linux-kernel\/","DOI":"10.1007\/978-3-030-30446-1_17"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"de Oliveira, D.B., Cucinotta, T., de Oliveira, R.S.: Untangling the intricacies of thread synchronization in the PREEMPT $$\\_$$ RT Linux Kernel. In: Proceedings of the IEEE 22nd International Symposium on Real-Time Distributed Computing (ISORC), Valencia, Spain, May 2019","DOI":"10.1109\/ISORC.2019.00012"},{"issue":"6","key":"17_CR34","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1002\/spe.2333","volume":"46","author":"DB Oliveira de","year":"2016","unstructured":"de Oliveira, D.B., de Oliveira, R.S.: Timing analysis of the PREEMPT $$\\_$$ RT Linux kernel. Softw.: Pract. Exp. 46(6), 789\u2013819 (2016). https:\/\/doi.org\/10.1002\/spe.2333","journal-title":"Softw.: Pract. Exp."},{"key":"17_CR35","unstructured":"Phoronix Test Suite: Open-source, automated benchmarking, May 2019. www.phoronix-test-suite.com"},{"key":"17_CR36","unstructured":"Poimboeuf, J.: Introducing kpatch: dynamic kernel patching, February 2014. https:\/\/www.redhat.com\/en\/blog\/introducing-kpatch-dynamic-kernel-patching"},{"key":"17_CR37","volume-title":"Software Fault Tolerance Techniques and Implementation","author":"LL Pullum","year":"2001","unstructured":"Pullum, L.L.: Software Fault Tolerance Techniques and Implementation. Artech House Inc., Norwood (2001)"},{"key":"17_CR38","unstructured":"Rostedt, S.: Secrets of the Ftrace function tracer. Linux Weekly News, January 2010. http:\/\/lwn.net\/Articles\/370423\/ . Accessed 09 May 2017"},{"key":"17_CR39","unstructured":"San Vicente Guti\u00e9rrez, C., Usategui San Juan, L., Zamalloa Ugarte, I., Mayoral Vilches, V.: Real-time Linux communications: an evaluation of the Linux communication stack for real-time robotic applications, August 2018. https:\/\/arxiv.org\/pdf\/1808.10821.pdf"},{"key":"17_CR40","doi-asserted-by":"publisher","unstructured":"Shahpasand, R., Sedaghat, Y., Paydar, S.: Improving the stateful robustness testing of embedded real-time operating systems. In: 2016 6th International Conference on Computer and Knowledge Engineering (ICCKE), pp. 159\u2013164, October 2016. https:\/\/doi.org\/10.1109\/ICCKE.2016.7802133","DOI":"10.1109\/ICCKE.2016.7802133"},{"issue":"12","key":"17_CR41","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/MC.2012.191","volume":"45","author":"A Spear","year":"2012","unstructured":"Spear, A., Levy, M., Desnoyers, M.: Using tracing to solve the multicore system debug problem. Computer 45(12), 60\u201364 (2012). https:\/\/doi.org\/10.1109\/MC.2012.191","journal-title":"Computer"},{"key":"17_CR42","unstructured":"The Linux Foundation: Automotive grade Linux, May 2019. https:\/\/www.automotivelinux.org\/"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Proceedings of the Twenty-second IEEE\/ACM International Conference on Automated Software Engineering, ASE 2007, pp. 501\u2013504. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1321631.1321719","DOI":"10.1145\/1321631.1321719"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30446-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,6]],"date-time":"2019-12-06T15:01:32Z","timestamp":1575644492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30446-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030304454","9783030304461"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30446-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sefm2019.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"89","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}