Call For Presentations for the seL4 Summit 2024

Important Dates:

Abstracts due: ~~22 April 2024~~ 29 April 2024
Notification of decisions: 7 June 2024
Summit: 15-17 October 2024

Overview

The seL4 summit aims at gathering the seL4 community to learn, share, and connect:

learn about the seL4 technology, its latest progress, use, successes, challenges, plans;
share exciting seL4 development, research, experience, application in the real world;
connect with other seL4 developers, users, providers, supporters, potential partners, and enthusiasts.

The seL4 summit covers the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.

The seL4 summit 2024 will be in Sydney, Australia.

Topics

We solicit proposals on any seL4-related topic, in particular in the areas of:

seL4 on-going and planned R&D, mature or early stage:
- seL4 research efforts
- seL4 development efforts
- work-in-progress seL4 development
- student work on seL4
- new/missing/next-gen kernel mechanisms
- seL4-related roadmaps: what you plan to work on and when
- seL4 grand challenges
- OS frameworks and services
- seL4 userland with programming language support beyond C
- High performance systems based on seL4: pushing the boundaries
seL4 experience reports
- experience with deploying seL4 in the field, in commercial/deployed products
- experience with teaching seL4
- experience with seL4 in certification schemes and application of industry standards
- experience with “building a business case for using a verified kernel”
- experience with porting software from other OSes
seL4 and hardware
- ports to new hardware platforms or architectures
- multicore systems
- virtualisation
- new/proposed hardware features or architectures, which could also enable or broaden the scope of formal reasoning (e.g. about time protection)
- seL4 in embedded processors on FPGAs, and impact of assured separation
- IOMMU solutions for various hardware architectures and impact for seL4
seL4 and assurance:
- application-level verification leveraging seL4 proofs
- correctness, spatial separation, temporal separation, and real-time proofs
- formalised interface between or composition of kernel-level proofs and user-level proofs
- verification engineering at scale, scaling verification productivity
- security/safety impact/assurance/certification for an seL4-based system

Submission

If you would like to propose a talk, please upload an abstract of one page or less for your proposed talk by ~~22 April 2024~~ 29 April 2024 on the submission portal. Abstracts should indicate why the talk fits in the seL4 summit scope. Notifications of accepted presentations will be made by 7 June 2024.

If you'd love to hear about some specific work from other people in the community, we encourage you to reach out to them to incite them to submit a proposal. :-) Alternatively, let us know at summit@sel4.systems.

Open invitation for a 5-minute slot to talk about your seL4 deployment

The community loves to hear about the deployment of seL4. So, if you:

are selling an end-user product that has seL4 embedded within, or
have integrated an seL4-based system/component into a deployed system,

you are welcome to a 5-min slot at the summit to talk about it, regardless of whether you are submitting an abstract for a full presentation! Simply send a short description by email to summit@sel4.systems by .

Contact

If you have questions, please do not hesitate to contact the seL4 Foundation summit team at: summit@sel4.systems.