S. Amani, A. Hixon, Z. Chen, C. Rizkallah, P. Chubb et al., COGENT: Verifying highassurance file system implementations, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2016), pp.175-188

M. Aponte, P. Courtieu, Y. Moy, and M. Sango, Maximal and compositional pattern-based loop invariants, FM 2012: Formal Methods -18th International Symposium, pp.37-51, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126145

D. Bailey, E. Barszcz, J. T. Barton, D. S. Browning, R. L. Carter et al., The NAS parallel benchmarks summary and preliminary results, pp.158-165, 1991.

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi'c et al., Computer Aided Verification (CAV), vol.6806, pp.171-177, 2011.

F. Bobot, J. Filliâtre, C. Marché, A. Paskevich, and . Why3, Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

J. Bouron, PATCH] Fix bug in which the long term ULE load balancer is executed only once, 2017.

J. Bouron, S. Chevalley, B. Lepers, W. Zwaenepoel, R. Gouicem et al., The battle of the schedulers: FreeBSD ULE vs. Linux CFS, USENIX Annual Technical Conference (USENIX ATC), pp.85-96, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01853267

G. Buttazzo, Hard Real-Time Computing Systems, Predictable Scheduling Algorithms and Applications, 2011.

D. Carver, R. Gouicem, J. Lozi, J. Sopena, B. Lepers et al., Fork/wait and multicore frequency scaling, Workshop on Programming Languages and Operating Systems (PLOS), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02349987

F. Cerqeira, F. Stutz, and B. B. Brandenburg, PROSA: A case for readable mechanized schedulability analysis, Real-Time Systems (ECRTS), pp.273-284, 2016.

H. Chen, T. Chajed, A. Konradi, S. Wang, A. ?leri et al., Verifying a high-performance crash-safe file system using a tree specification, Symposium on Operating Systems Principles (SOSP, pp.270-286, 2017.

H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek et al., Using Crash Hoare logic for certifying the FSCQ file system, Symposium on Operating Systems Principles (SOSP) (2015), pp.18-37

T. Chen, L. I. Ananiev, and A. V. Tikhonov, Keeping kernel performance from regressions, Linux Symposium, vol.1, pp.93-102, 2007.

N. Chong and S. Ishtiaq, Reasoning about the ARM weakly consistent memory model, Workshop on Memory systems performance and correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.16-19, 2008.

S. Conchon, A. Coqereau, M. Iguernlala, and A. Mebsout, Alt-Ergo 2.2, SMT Workshop: International Workshop on Satisfiability Modulo Theories, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01960203

M. Dashti, A. Fedorova, J. Funston, F. Gaud, R. Lachaize et al., Traffic management: a holistic approach to memory placement on NUMA systems, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013), pp.381-394
URL : https://hal.archives-ouvertes.fr/hal-00945758

B. Delaware, C. Pit-claudel, J. Gross, A. Chlipala, and . Fiat, Deductive synthesis of abstract data types in a proof assistant, Principles of Programming languages (POPL, pp.689-700, 2015.

P. Deligiannis, A. F. Donaldson, and Z. Rakamaric, Fast and precise symbolic analysis of concurrency bugs in device drivers, Automated Software Engineering (ASE, pp.166-177, 2015.

M. Dobrescu, A. , and K. , Software dataplane verification, Communications of the ACM, vol.58, pp.113-121, 2015.

D. Engler and K. Ashcraft, RacerX: Effective, static detection of race conditions and deadlocks, Symposium on Operating Systems Principles (SOSP, pp.237-252, 2003.

J. Erickson, M. Musuvathi, S. Burckhardt, and K. Olynyk, Effective data-race detection for the kernel, Operating Systems Design and Implementation (OSDI) (2010), pp.151-162

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, vol.48, pp.152-174, 2016.

C. Frost, M. Mammarella, E. Kohler, A. De-los-reyes, S. Hovsepian et al., Generalized file system dependencies, Symposium on Operating Systems Principles (SOSP, pp.307-320, 2007.

R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim et al., CertiKOS: an extensible architecture for building certified concurrent OS kernels, Operating Systems Design and Implementation (OSDI, pp.653-669, 2016.

C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno et al., Ironfleet: proving practical distributed systems correct, Symposium on Operating Systems Principles (SOSP, pp.1-17, 2015.

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno et al., Ironclad apps: End-to-end security via automated full-system verification, Operating Systems Design and Implementation (OSDI) (2014), vol.14, pp.165-181

F. Hermenier and L. Henrio, Trustable virtual machine scheduling in a cloud, Symposium on Cloud Computing (SOCC, pp.15-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01627906

S. Kanev, J. P. Darago, K. Hazelwood, P. Ranganathan, T. Moseley et al., Profiling a warehouse-scale computer, International Symposium on Computer Architecture (ISCA, pp.158-169, 2015.

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., seL4: formal verification of an OS kernel, Symposium on Operating Systems Principles (SOSP, pp.207-220, 2009.

V. Kuncak, Developing verified software using Leon, NASA Formal Methods (NFM) (2015), pp.12-15

K. Leino and M. Rustan, Dafny: An automatic program verifier for functional correctness, International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2010), pp.348-370

B. Lepers, W. Zwaenepoel, J. Lozi, N. Palix, R. Gouicem et al., Towards proving optimistic multicore schedulers, Workshop on Hot Topics in Operating Systems (HotOS, pp.18-23, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01556597

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Principles of Programming languages (POPL, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

, Linux test project, 2012.

X. Liu, Z. Guo, X. Wang, F. Chen, X. Lian et al., D 3 S: debugging deployed distributed systems, Networked Systems Design and Implementation (NSDI, pp.423-437, 2008.

J. Lozi, B. Lepers, J. Funston, F. Gaud, V. Quéma et al., The Linux scheduler: a decade of wasted cores, European Conference on Computer Systems (EuroSys), vol.1, p.16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01295194

H. Mai, E. Pek, H. Xue, S. T. King, and P. Madhusudan, Verifying security invariants in ExpressOS, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013), pp.293-304

F. Mérillon, L. Réveillère, C. Consel, R. Marlet, and G. Muller, Devil: An IDL for hardware programming, Operating Systems Design and Implementation (OSDI, pp.17-30, 2000.

G. Muller, C. Consel, R. Marlet, L. P. Barreto, F. Merillon et al., Towards robust OSes for appliances: A new approach based on domain-specific languages, ACM SIGOPS European workshop, pp.19-24, 2000.
URL : https://hal.archives-ouvertes.fr/hal-00350228

G. Muller, J. L. Lawall, and H. Duchesne, A framework for simplifying the development of kernel schedulers: Design and performance evaluation, High-Assurance Systems Engineering (HASE), pp.56-65, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00457120

M. Musuvathi, D. Y. Park, A. Chou, D. R. Engler, and D. L. Dill, CMC: a pragmatic approach to model checking real code, Operating Systems Design and Implementation (OSDI, pp.75-88, 2002.

L. Nelson, H. Sigurbjarnarson, K. Zhang, D. Johnson, J. Bornholt et al., Hyperkernel: Push-button verification of an OS kernel, Symposium on Operating Systems Principles (SOSP, pp.252-269, 2017.

S. E. Perl and W. E. Weihl, Performance assertion checking, Symposium on Operating Systems Principles (SOSP) (1993), pp.134-145

S. K. Sahoo, J. Criswell, C. Geigle, A. , and V. , Using likely invariants for automated software fault localization, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013), pp.139-152

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, A. et al., Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), vol.15, pp.391-411, 1997.

, Scheduler domains

A. Schüpbach, S. Peter, A. Baumann, T. Roscoe, P. Barham et al., Embracing diversity in the Barrelfish manycore operating system, Workshop on Managed Many-Core Systems, vol.27, 2008.

K. Shen, M. Zhong, L. , and C. , I/O system performance debugging using model-driven anomaly characterization, File and Storage Technologies (FAST) (2005), pp.309-322

H. Sigurbjarnarson, J. Bornholt, E. Torlak, W. , and X. , Pushbutton verification of file systems via crash refinement, Operating Systems Design and Implementation (OSDI, pp.1-16, 2016.

D. Sites, Data center computers: Modern challenges in CPU design, vol.56, p.32, 2015.

. Sysbench,

V. Vojdani, K. Apinis, V. Rõtov, H. Seidl, V. Vene et al., Static race detection for device drivers: The Goblint approach, Automated Software Engineering (ASE), pp.391-402, 2016.

C. A. Waldspurger and W. E. Weihl, Lottery scheduling: Flexible proportional-share resource management, Operating Systems Design and Implementation (OSDI), pp.1-11, 1994.

M. Wand, Continuation-based multiprocessing, LISP and Functional Programming, pp.19-28, 1980.

J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang et al., Verdi: a framework for implementing and formally verifying distributed systems, In Programming Language Design and Implementation, pp.357-368, 2015.

C. Xu and F. C. Lau, Load balancing in parallel computers: theory and practice, vol.381, 1996.

J. Yang, P. Twohey, D. Engler, and M. Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), vol.24, pp.393-423, 2006.