COGENT: Verifying highassurance file system implementations, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2016), pp.175-188 ,
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
The NAS parallel benchmarks summary and preliminary results, pp.158-165, 1991. ,
, Computer Aided Verification (CAV), vol.6806, pp.171-177, 2011.
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
PATCH] Fix bug in which the long term ULE load balancer is executed only once, 2017. ,
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
Hard Real-Time Computing Systems, Predictable Scheduling Algorithms and Applications, 2011. ,
Fork/wait and multicore frequency scaling, Workshop on Programming Languages and Operating Systems (PLOS), 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02349987
PROSA: A case for readable mechanized schedulability analysis, Real-Time Systems (ECRTS), pp.273-284, 2016. ,
Verifying a high-performance crash-safe file system using a tree specification, Symposium on Operating Systems Principles (SOSP, pp.270-286, 2017. ,
Using Crash Hoare logic for certifying the FSCQ file system, Symposium on Operating Systems Principles (SOSP) (2015), pp.18-37 ,
Keeping kernel performance from regressions, Linux Symposium, vol.1, pp.93-102, 2007. ,
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. ,
Alt-Ergo 2.2, SMT Workshop: International Workshop on Satisfiability Modulo Theories, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01960203
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
Deductive synthesis of abstract data types in a proof assistant, Principles of Programming languages (POPL, pp.689-700, 2015. ,
Fast and precise symbolic analysis of concurrency bugs in device drivers, Automated Software Engineering (ASE, pp.166-177, 2015. ,
Software dataplane verification, Communications of the ACM, vol.58, pp.113-121, 2015. ,
RacerX: Effective, static detection of race conditions and deadlocks, Symposium on Operating Systems Principles (SOSP, pp.237-252, 2003. ,
Effective data-race detection for the kernel, Operating Systems Design and Implementation (OSDI) (2010), pp.151-162 ,
The spirit of ghost code, Formal Methods in System Design, vol.48, pp.152-174, 2016. ,
Generalized file system dependencies, Symposium on Operating Systems Principles (SOSP, pp.307-320, 2007. ,
CertiKOS: an extensible architecture for building certified concurrent OS kernels, Operating Systems Design and Implementation (OSDI, pp.653-669, 2016. ,
Ironfleet: proving practical distributed systems correct, Symposium on Operating Systems Principles (SOSP, pp.1-17, 2015. ,
Ironclad apps: End-to-end security via automated full-system verification, Operating Systems Design and Implementation (OSDI) (2014), vol.14, pp.165-181 ,
Trustable virtual machine scheduling in a cloud, Symposium on Cloud Computing (SOCC, pp.15-26, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01627906
Profiling a warehouse-scale computer, International Symposium on Computer Architecture (ISCA, pp.158-169, 2015. ,
seL4: formal verification of an OS kernel, Symposium on Operating Systems Principles (SOSP, pp.207-220, 2009. ,
Developing verified software using Leon, NASA Formal Methods (NFM) (2015), pp.12-15 ,
Dafny: An automatic program verifier for functional correctness, International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2010), pp.348-370 ,
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
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.
D 3 S: debugging deployed distributed systems, Networked Systems Design and Implementation (NSDI, pp.423-437, 2008. ,
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
Verifying security invariants in ExpressOS, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013), pp.293-304 ,
Devil: An IDL for hardware programming, Operating Systems Design and Implementation (OSDI, pp.17-30, 2000. ,
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
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
CMC: a pragmatic approach to model checking real code, Operating Systems Design and Implementation (OSDI, pp.75-88, 2002. ,
Hyperkernel: Push-button verification of an OS kernel, Symposium on Operating Systems Principles (SOSP, pp.252-269, 2017. ,
Performance assertion checking, Symposium on Operating Systems Principles (SOSP) (1993), pp.134-145 ,
Using likely invariants for automated software fault localization, Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013), pp.139-152 ,
Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), vol.15, pp.391-411, 1997. ,
, Scheduler domains
Embracing diversity in the Barrelfish manycore operating system, Workshop on Managed Many-Core Systems, vol.27, 2008. ,
I/O system performance debugging using model-driven anomaly characterization, File and Storage Technologies (FAST) (2005), pp.309-322 ,
Pushbutton verification of file systems via crash refinement, Operating Systems Design and Implementation (OSDI, pp.1-16, 2016. ,
Data center computers: Modern challenges in CPU design, vol.56, p.32, 2015. ,
,
Static race detection for device drivers: The Goblint approach, Automated Software Engineering (ASE), pp.391-402, 2016. ,
Lottery scheduling: Flexible proportional-share resource management, Operating Systems Design and Implementation (OSDI), pp.1-11, 1994. ,
Continuation-based multiprocessing, LISP and Functional Programming, pp.19-28, 1980. ,
Verdi: a framework for implementing and formally verifying distributed systems, In Programming Language Design and Implementation, pp.357-368, 2015. ,
, Load balancing in parallel computers: theory and practice, vol.381, 1996.
Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), vol.24, pp.393-423, 2006. ,